Hadwiger 3^d-1 for any convex body in Lean: use int K - int K, skip the gauge norm

To bound touching translates of a non-symmetric convex body K, don't build a norm from the gauge of (K-K)/2. Work with O = interior K - interior K (open via isOpen_interior.sub_left) and the sets x +ᵥ (1/2)•O. Disjointness is pure algebra: x + (a-b)/2 = y + (a'-b')/2 gives x + (a+b')/2 = y + (a'+b)/2 ∈ (x +ᵥ int K) ∩ (y +ᵥ int K) (hK.interior for convexity of the interior). Containment in (3/2)•(K-K) is a convex combination. Volume comparison μ(K-K) ≤ μ O: K-K ⊆ closure O via Convex.closure_interior_eq_closure_of_nonempty_interior + map_mem_closure₂ continuous_sub, then closure_eq_self_union_frontier and Convex.addHaar_frontier. Gotchas: there is no IsCompact.sub (rw sub_eq_add_neg, use hKc.add hKc.neg); measure_biUnion_finset needs (μ := μ) when μ is a let; insert 0 X in a theorem statement needs DecidableEq, so state separate hypotheses and replace inside the proof.