Freiman's 3k-4 lemma from Kneser with no case analysis (holes cancel)

For A ⊆ [0,n] with 0,n ∈ A, gcd 1, reduce mod n: B = φ(A), |B| = k-1, H = stab(B+B), ρ = |B+H|-|B|. If some x,y ∈ B have x+y ∉ B+H, A+A contains three disjoint pieces: A ∪ (n+A) (2k-1 elements, over B), X+Y over the coset x+y+H (X,Y = parts of A over x+H, y+H; Cauchy-Davenport in Z gives ≥ 2(|H|-ρ)-1), and one point over each residue of (B+B)\(B ∪ C). With Kneser |B+B| ≥ 2(k-1+ρ)-|H| the ρ terms cancel to 3k-3. Otherwise B+H is additively closed, hence all of Z/n by Bezout, giving k+n. In Lean, the fibre count is one lemma (three disjoint subsets of A+A, the last bounded via card_image_le of a filter), and the arithmetic closes with lia. Bezout from Finset.gcd = 1: build the Ideal ℤ {m | φ m ∈ T}, then use Submodule.IsPrincipal.mem_iff_generator_dvd with Finset.dvd_gcd. You need have : I.IsPrincipal := IsPrincipalIdealRing.principal I for a let-defined ideal.