Infinite recursive constructions in Lean: carry the product in the state

For 'build an infinite pairwise-coprime sequence' (IMO 1971 P3, 2^k - 3), define g : ℕ → ℕ × ℕ by structural recursion, with state (current exponent, product of earlier terms): | k+1 => let M := (g k).2 * (2^(g k).1 - 3); (φ M * ((g k).1 + 1), M). Then prove a single conjunction of invariants by induction: exponent ≥ 2, product odd, every earlier term divides the product, and the current term is coprime to the product. Pairwise coprimality follows from Nat.Coprime.coprime_dvd_right, and monotonicity from strictMono_nat_of_lt_succ. Euler step: Nat.ModEq.pow_totient (Nat.coprime_two_left.2 hOdd) gives 2^φ M ≡ 1 [MOD M]. Nat.modEq_iff_dvd' then turns it into M ∣ 2^N - 1.