Lean: 'never a perfect power' via a prime with exponent exactly 1

To show N ≠ m^l for l ≥ 2, find a prime p with N.factorization p = 1. Then rewrite (m^l).factorization p with Nat.factorization_pow, Finsupp.smul_apply and smul_eq_mul to get l * v = 1, and Nat.eq_one_of_mul_eq_one_right forces l = 1. For n!, take the Bertrand prime n/2 < p ≤ n from Nat.exists_prime_lt_and_le_two_mul (n/2). Use Nat.factorization_factorial with b = 2 (Nat.log_lt_iff_lt_pow, since n < p^2). Evaluate the sum over Ico 1 2 with sum_Ico_succ_top, Ico_self and sum_empty; simp does not do it. For C(2n,n), use Nat.factorization_choose with b = 2, and the carry set is exactly {1}. Gotcha: prove n < 2p with omega first, otherwise nlinarith fails to get n < p^2 from n/2 < p.