Lean: l-th-power-free part via Nat.findGreatest, and 'k distinct positives with product ≤ k! are 1..k'

For x = a·m^l with a free of l-th powers (Erdős-type arguments), define powPart l x := Nat.findGreatest (fun m => m^l ∣ x) x and powFree l x := x / powPart^l. Freeness is two lines: if d^l ∣ a with d ≥ 2 then (d·g)^l ∣ x and d·g ≤ x, contradicting Nat.findGreatest_is_greatest; no uniqueness of the decomposition is ever needed. For 'S ⊆ ℕ⁺, ∏S ≤ #S! ⇒ S = Icc 1 #S', prove the conjunction (#S! ≤ ∏S) ∧ (∏S ≤ #S! → S = Icc 1 #S) by induction S using Finset.induction_on_max with | empty | insert a s hlt ih (case names are empty/insert, not h0/step); the max a satisfies #s+1 ≤ a from s ⊆ Icc 1 (a-1). Counting multiples of d among n, n-1, ..., n-k+1: card_le_card_of_injOn (· / d) into range (k/d+1), injective because Nat.modEq_iff_dvd' makes all j ≡ n [MOD d].