English
For n ≥ 2, for all k,i with k = 2i+3, and given that every divisor m of n with m≥2 satisfies k ≤ m, then minFacProp(n, n.minFacAux(k)).
Русский
Пусть n ≥ 2, для любых k,i с k = 2i+3 и при условии, что каждый делитель m n с m≥2 удовлетворяет k ≤ m, тогда minFacProp(n, n.minFacAux(k)).
LaTeX
$$$\\\\forall n \\\\ge 2, \\\\forall k,i \\\\in \\\\mathbb{N}, \\\\text{if } k = 2i+3 \\\\Rightarrow (\\\\forall m \\\\in \\\\mathbb{N}, 2 \\\\le m \\\\land m \\\\mid n \\\\Rightarrow k \\\\le m) \\\\Rightarrow \\\\operatorname{minFacProp}(n, n.minFacAux(k)).$$$
Lean4
theorem minFacAux_has_prop {n : ℕ} (n2 : 2 ≤ n) :
∀ k i, k = 2 * i + 3 → (∀ m, 2 ≤ m → m ∣ n → k ≤ m) → minFacProp n (minFacAux n k)
| k => fun i e a => by
rw [minFacAux]
by_cases h : n < k * k
· have pp : Prime n :=
prime_def_le_sqrt.2 ⟨n2, fun m m2 l d => not_lt_of_ge l <| lt_of_lt_of_le (sqrt_lt.2 h) (a m m2 d)⟩
simpa only [k, h] using ⟨n2, dvd_rfl, fun m m2 d => le_of_eq ((dvd_prime_two_le pp m2).1 d).symm⟩
have k2 : 2 ≤ k := by
subst e
apply Nat.le_add_left
simp only [k, h, ↓reduceIte]
by_cases dk : k ∣ n <;> simp only [k, dk, ↓reduceIte]
· exact ⟨k2, dk, a⟩
· refine
have := minFac_lemma n k h
minFacAux_has_prop n2 (k + 2) (i + 1) (by simp [k, e, Nat.left_distrib, add_right_comm]) fun m m2 d => ?_
rcases Nat.eq_or_lt_of_le (a m m2 d) with me | ml
· subst me
contradiction
apply (Nat.eq_or_lt_of_le ml).resolve_left
intro me
rw [← me, e] at d
have d' : 2 * (i + 2) ∣ n := d
have := a _ le_rfl (dvd_of_mul_right_dvd d')
rw [e] at this
exact absurd this (by contradiction)
termination_by k => sqrt n + 2 - k
