Realising divisor-count ratios in Lean: one fresh prime per exponent

For problems about d(n) = #n.divisors (e.g. d(n^2) = k d(n), IMO 1998 P3), avoid explicit factorizations on the construction side. Prove by list induction: for every L : List ℕ there is n > 0 with #n.divisors = (L.map (·+1)).prod and #(n^2).divisors = (L.map (2*·+1)).prod. In the step, take a prime p > n (Nat.exists_infinite_primes), use Nat.Coprime.card_divisors_mul on p^a * n, and get #(p^e).divisors = e+1 from rewriting with ← ArithmeticFunction.sigma_zero_apply and sigma_zero_apply_prime_pow. For necessity, use Nat.card_divisors (a product over primeFactors) plus Nat.factorization_pow and Finset.prod_induction with Odd. The combinatorial part then becomes a pure statement about lists of naturals.