English
Let n be a natural number. If a bounds all prime divisors of n, then the list consisting of a followed by primeFactorsList(n) is totally ordered by ≤.
Русский
Пусть n — натуральное число. Если a верхняя граница для всех простых делителей n, то список a :: primeFactorsList(n) упорядочен по ≤.
LaTeX
$$$ \forall n\,( \forall p,\ \text{Prime}(p) \rightarrow p \mid n \rightarrow a \le p) \rightarrow \text{List.IsChain}( (\le) ) (a :: \text{primeFactorsList}(n)) $$$
Lean4
theorem isChain_cons_primeFactorsList {n : ℕ} :
∀ {a}, (∀ p, Prime p → p ∣ n → a ≤ p) → List.IsChain (· ≤ ·) (a :: primeFactorsList n) := by
match n with
| 0 => simp
| 1 => simp
| k + 2 =>
intro a h
let m := minFac (k + 2)
have : (k + 2) / m < (k + 2) := factors_lemma
rw [primeFactorsList]
refine List.IsChain.cons_cons ((le_minFac.2 h).resolve_left (by simp)) (isChain_cons_primeFactorsList ?_)
exact fun p pp d => minFac_le_of_dvd pp.two_le (d.trans <| div_dvd_of_dvd <| minFac_dvd _)
