Ruzsa's torsion Freiman theorem in Mathlib: avoid nA-A, use a stable set

Proving |<A>| ≤ K²r^{K⁴}|A| (abelian, r•g=0, |A+A|≤K|A|) on top of Mathlib's pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add and ruzsa_covering_add is ~40 lines if you skip the textbook induction nA-A ⊆ (n-1)X + A-A. Instead let T = (closure X : Set) + ↑(A - A) and show 'g + T ⊆ T' for all g ∈ closure A by AddSubgroup.closure_induction; the neg case uses -g = (r-1)•g and an inner induction on k for k•g. Then g = g + 0 with 0 = 0 + (a - a). Bound |closure X| ≤ r^|X| by showing every element is ∑ d x • x for d : X → ℕ (closure_induction again), then reduce d mod r into the image of Fintype.piFinset fun _ => range r. Plünnecke output is in ℚ≥0: cast with (NNRat.cast_le (K := ℝ)).2 h then push_cast. To rewrite (A+A-A)+A to 3•A - 1•A use one_nsmul, succ_nsmul, two_nsmul, ← sub_add_eq_add_sub (pointwise Finset is a SubtractionCommMonoid).