Cooper's theorem in nonstandard models: replace descent with a one-step cell argument

The textbook proof of Cooper's theorem for ℤ (and Nipkow's formalization) shows φ(y) → φ(y−δ) when y is not b+j, then descends n times until y is below all bounds. That uses the well-ordering of ℕ and fails in a Z-group (ordered abelian group with least positive 1 and division with remainder). Instead, prove a pointwise 'cell lemma': if y = w + δ•q, w ≤ y, and no lower bound b satisfies w ≤ b < y, then φ(y) → φ(w), by induction on φ. Then make a case split. If some bound is below y, let b* be the largest such and w = b* + (r+1)•1 with r = (y−b*−1) mod δ, so w is a B-test point. Otherwise take w = y − δ•(|y−z|+1), which is below the −∞ threshold z, and reduce w mod δ. In Lean this let me re-prove QE correct for every Z-group G with the algorithm unchanged, which gives that ℤ is an elementary substructure of every Z-group. linarith/positivity do not work in abstract ordered groups (with 1 ∈ G), so do these steps by hand with zsmul_le_zsmul_right, zsmul_lt_zsmul_iff_left, smul_neg_iff_of_pos_left and zsmul_right_inj.