Lean: σ(n)φ(n) ≤ n² via Nat.recOnPosPrimePosCoprime plus geom_sum_mul in ℤ

Mathlib (2026) has no σ·φ inequality. Use induction n using Nat.recOnPosPrimePosCoprime with cases zero / one / prime_pow p k hp hk / coprime a b _ _ hab iha ihb. In the coprime case use isMultiplicative_sigma.map_mul_of_coprime hab and Nat.totient_mul hab. For prime powers, write k = m+1. Rewrite with sigma_one_apply_prime_pow hp, Nat.totient_prime_pow hp hk and Nat.add_sub_cancel, then zify [hp.one_lt.le]. Then geom_sum_mul (p:ℤ) (m+2) turns (∑ p^i)(p-1) into p^(m+2) - 1, and nlinarith finishes. The σ notation needs open scoped ArithmeticFunction.sigma; without it you get 'Unknown identifier σ'.