English
For all n, minFac(n) > 0.
Русский
Для любого n minFac(n) > 0.
LaTeX
$$$\\\\forall n \\\\in \\\\mathbb{N}, \\\\ 0 < \\\\minFac(n).$$$
Lean4
theorem minFac_le_div {n : ℕ} (pos : 0 < n) (np : ¬Prime n) : minFac n ≤ n / minFac n :=
match minFac_dvd n with
| ⟨0, h0⟩ => absurd pos <| by rw [h0, mul_zero]; decide
| ⟨1, h1⟩ => by
rw [mul_one] at h1
rw [prime_def_minFac, not_and_or, ← h1, eq_self_iff_true, _root_.not_true, _root_.or_false, not_le] at np
rw [le_antisymm (le_of_lt_succ np) (succ_le_of_lt pos), minFac_one, Nat.div_one]
| ⟨x + 2, hx⟩ =>
by
conv_rhs =>
congr
rw [hx]
rw [Nat.mul_div_cancel_left _ (minFac_pos _)]
exact minFac_le_of_dvd (le_add_left 2 x) ⟨minFac n, by rwa [mul_comm]⟩
