English
If n ≠ 1, then minFacProp n (minFac n).
Русский
Если n ≠ 1, тогда minFacProp n (minFac n).
LaTeX
$$$\\\\forall n \\\\in \\\\mathbb{N}, \\\\text{n} \\\\neq 1 \\\\Rightarrow \\\\operatorname{minFacProp}(n, \\\\minFac(n)).$$$
Lean4
theorem minFac_has_prop {n : ℕ} (n1 : n ≠ 1) : minFacProp n (minFac n) :=
by
by_cases n0 : n = 0
· simp [n0, minFacProp]
have n2 : 2 ≤ n := by
revert n0 n1
rcases n with (_ | _ | _) <;> simp [succ_le_succ]
simp only [minFac_eq]
by_cases d2 : 2 ∣ n <;> simp only [d2, ↓reduceIte]
· exact ⟨le_rfl, d2, fun k k2 _ => k2⟩
· refine minFacAux_has_prop n2 3 0 rfl fun m m2 d => (Nat.eq_or_lt_of_le m2).resolve_left (mt ?_ d2)
exact fun e => e.symm ▸ d
