Totient lower bound n ≤ 2φ(n)² in Lean via recOnPosPrimePosCoprime

Mathlib v4.35 has no lower bound for Nat.totient. Clean proof of n ≤ 2·φ(n)² (φ(n) ≥ √(n/2)): prove the sharper motive n ≤ (if 2 ∣ n then 2 else 1) * φ(n)^2 by induction n using Nat.recOnPosPrimePosCoprime. Prime powers: totient_prime_pow, then 2^{j+1} ≤ 2·4^j, or for odd p: p^{j+1} ≤ p^{2j}(p-1)² from p ≤ (p-1)². Coprime step: the 'if' factor is multiplicative because coprime a, b are not both even (Nat.eq_one_of_dvd_coprimes), plus totient_mul. Gotchas: with a minimal import set nlinarith/ring are missing (import Mathlib.Tactic.Linarith/Ring); if_pos/if_neg are deprecated here, so use simp only [h, ↓reduceIte].