English
For n ≥ 2 and any k = 2i+3, if every divisor m of n with m ≥ 2 satisfies k ≤ m, then minFacProp(n, minFacAux(n, k)).
Русский
Пусть n ≥ 2; для любого k = 2i+3, если каждый делитель m числа n с m ≥ 2 удовлетворяет k ≤ m, то minFacProp(n, minFacAux(n, k)).
LaTeX
$$$\\\\forall n \\\\ge 2, \\\\forall k,i \\\\in \\\\mathbb{N}, \\\\text{if } k = 2i+3 \\\\text{ and } (\\\\forall m \\\\in \\\\mathbb{N}, 2 \\\\le m \\\\land m \\\\mid n \\\\Rightarrow k \\\\le m) \\\\text{ then } \\\\operatorname{minFacProp}(n, \\\\operatorname{minFacAux}(n, k)).$$$
Lean4
/-- If `n < k * k`, then `minFacAux n k = n`, if `k | n`, then `minFacAux n k = k`.
Otherwise, `minFacAux n k = minFacAux n (k+2)` using well-founded recursion.
If `n` is odd and `1 < n`, then `minFacAux n 3` is the smallest prime factor of `n`.
This definition is by well-founded recursion, so `rfl` or `decide` cannot be used.
One can use `norm_num` to prove `Nat.prime n` for small `n`.
-/
def minFacAux (n : ℕ) : ℕ → ℕ
| k => if n < k * k then n else if k ∣ n then k else minFacAux n (k + 2)
termination_by k => sqrt n + 2 - k
decreasing_by simp_wf; apply minFac_lemma n k; assumption
