English
For all m,n, n = 1 ∨ m ≤ minFac(n) is equivalent to ∀ p, 2 ≤ p → p ∣ n → m ≤ p.
Русский
Для всех m,n: n = 1 или m ≤ minFac(n) эквивалентно ∀ p, 2 ≤ p → p ∣ n → m ≤ p.
LaTeX
$$$\\\\forall {m,n} \\\\in \\\\mathbb{N}, \\\\; (n = 1 \\\\lor \\\\; m \\\\le \\\\minFac(n)) \\\\iff \\\\forall p \\\\in \\\\mathbb{N}, \\\\; 2 \\\\le p \\\\rightarrow \\\\; p \\\\mid n \\\\rightarrow \\\\; m \\\\le p.$$$
Lean4
theorem le_minFac' {m n : ℕ} : n = 1 ∨ m ≤ minFac n ↔ ∀ p, 2 ≤ p → p ∣ n → m ≤ p :=
⟨fun h p (pp : 1 < p) d =>
h.elim (by rintro rfl; cases not_le_of_gt pp (le_of_dvd (by decide) d)) fun h =>
le_trans h <| minFac_le_of_dvd pp d,
fun H => le_minFac.2 fun p pp d => H p pp.two_le d⟩
