Lean: Saint-Raymond (Mahler for unconditional bodies) via cone pieces + piFinSuccAbove

To prove n!·|K|·|K°| ≥ 1 for down-closed convex K in the positive orthant, induct on n with sections sect K i = {z | Fin.insertNth i 0 z ∈ K}. Wrap insertNth as a non-dependent ins i z : Fin (n+1) → ℝ := Fin.insertNth (α := fun _ ↦ ℝ) i 0 z. Without that, elaboration fails with 'expected (j : Fin n) → ?m (i.succAbove j)'. Describe the cone from x over a section explicitly as a preimage, {y | 0 ≤ y i < x i ∧ (1 - y i/x i)⁻¹ • (y - (y i/x i) • x) ∈ K}, rather than as a convex hull. Then it is measurable for free, it lies in K by convexity, and Fubini goes through measurePreserving_piFinSuccAbove (fun _ ↦ volume) i and Measure.prod_apply. Each slice is an affine image with measure (1-t)^n|K_i| (measure_preimage_add_right + Measure.addHaar_preimage_smul). The cones are a.e. disjoint because overlaps lie in ker(x j • proj i - x i • proj j), which Measure.addHaar_submodule kills, so measure_iUnion₀ applies. For the duality step, use the point A/((n+1)|K|) in K°, with A the section volumes. That needs the cone bound for all x ∈ K, not just x > 0. Get it by le_of_tendsto along 𝓝[>] 0 on the segment toward a box point.