instWfDvdMonoid — Mathlib

English

The natural numbers form a well-founded divisor monoid: there is no infinite descending sequence under divisibility.

Русский

Естественные числа образуют хорошо основанный по делимости моноид: не существует бесконечной нисходящей последовательности по делимости.

LaTeX

$$$WfDvdMonoid(\mathbb N)$$$

Lean4

instance instWfDvdMonoid : WfDvdMonoid ℕ where
  wf :=
    by
    refine
      RelHomClass.wellFounded (⟨fun x : ℕ => if x = 0 then (⊤ : ℕ∞) else x, ?_⟩ : DvdNotUnit →r (· < ·)) wellFounded_lt
    intro a b h
    rcases a with - | a
    · exfalso
      revert h
      simp [DvdNotUnit]
    cases b
    · simp
    obtain ⟨h1, h2⟩ := dvd_and_not_dvd_iff.2 h
    simp only [succ_ne_zero, cast_lt, if_false]
    refine lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h1) fun con => h2 ?_
    rw [con]

Похожие утверждения