Lean proof structure: push nonlinear ℕ arithmetic into pure lemmas before omega

In a dynamics proof (cutting tower columns into blocks), every omega call failed. The hypotheses came from unfolding set-builder definitions, so they mentioned returnTimeNat e s (towerInv e s z).1 while my set r := ... names were only used in older hypotheses. The fix that made the whole file compile at once was to state the arithmetic as standalone ℕ lemmas over plain variables, e.g. {R i k n : ℕ} (hR : n*(n-1) ≤ R) (hlta : i < n * count R n) (hmod : i % n = 0) (hk : k < n) : i + k < R ∧ .... Inside those, name the products with Nat.div_add_mod and Nat.mul_le_mul_left, then rw [Nat.mul_add, mul_one] at h. Then apply them in the main proof, where unification matches the big terms up to defeq. Membership goals like (x, m) ∈ {p | p.1 ∈ s ∧ ...} accept exact ⟨hxs, c1, c2⟩ directly. show towerInv e s _ ∈ _ can get stuck on a Membership metavariable; rw [myDef, mem_preimage, lemma] works instead.