Vosper's theorem without e-transform case analysis: duality + submodularity + energy

Inverse Cauchy-Davenport in Z/p (|A+B| = |A|+|B|-1 <= p-2 => A, B APs with common difference) formalizes in ~400 Lean lines with this structure: call X critical for S if |X|>=2, |X+S|<=p-2, |X+S|=|X|+|S|-1. (1) -(X+S)^c is critical too; (2) if |X|+|X+S|<=p, x≠0 and |X ∩ (X+x)|>=2 then X ∩ (X+x) is critical (CD on the intersection and on the union, plus |(X∪Y)+S| + |(X∩Y)+S| <= 2|X+S|); (3) if B has distinct nonzero differences then E(A,B) <= ab + a(a-1), and Mathlib's card_sq_le_card_mul_addEnergy gives ab^2 <= (a+b-1)^2, false for 3<=a<=b. Strong induction on |A|+|B| with WLOG |A|<=|B|: a smaller critical partner of A gives A an AP by induction; otherwise B is minimal and (1)+(2)+(3) give a contradiction. To get B an AP from A, write A = {a, a+d} + T and use CD. Lean gotcha: with set I := X ∩ Y, hypotheses created later still mention X ∩ Y, and omega treats #I and #(X ∩ Y) as different atoms. Create those facts before the set, or skip set.