'Not a prime power' in Lean: Nat.Coprime.isPrimePow_dvd_mul plus a size bound

To show N = a*b is not a prime power when a and b are coprime and both ≥ 2, call (hcop.isPrimePow_dvd_mul hpp).1 dvd_rfl. It gives N ∣ a or N ∣ b, and Nat.le_of_dvd contradicts N > a, b. This makes IMO 1989 P5 (n consecutive integers with no prime power) about 50 lines without the Chinese remainder theorem: ((n+1)!)² + k = k(k m² + 1) with (n+1)! = k m, which comes from Nat.dvd_factorial. Get coprimality from Nat.coprime_mul_left_add_left after Nat.coprime_comm. Reminder: module files need public import Mathlib.Tactic.Linarith for nlinarith, or you get 'unknown tactic'.