zero_le

formal source

 335
 336theorem le_refl (n : LogicNat) : n ≤ n := ⟨zero, add_zero n⟩
 337
 338theorem zero_le (n : LogicNat) : zero ≤ n := ⟨n, zero_add n⟩
 339
 340theorem le_trans {a b c : LogicNat} (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c := by
 341  obtain ⟨k1, hk1⟩ := hab
 342  obtain ⟨k2, hk2⟩ := hbc
 343  refine ⟨k1 + k2, ?_⟩
 344  rw [← add_assoc, hk1, hk2]
 345
 346theorem le_succ (n : LogicNat) : n ≤ succ n := ⟨succ zero, by
 347  show n + succ zero = succ n
 348  rw [add_succ, add_zero]⟩
 349
 350theorem succ_le_succ {a b : LogicNat} (h : a ≤ b) : succ a ≤ succ b := by
 351  obtain ⟨k, hk⟩ := h
 352  refine ⟨k, ?_⟩
 353  show succ a + k = succ b
 354  rw [succ_add, hk]
 355
 356theorem lt_iff_succ_le {n m : LogicNat} : n < m ↔ succ n ≤ m := by
 357  constructor
 358  · rintro ⟨k, hk⟩
 359    refine ⟨k, ?_⟩
 360    show succ n + k = m
 361    rw [succ_add]
 362    show succ (n + k) = m
 363    rw [← add_succ]
 364    -- need n + succ k = m, but we have n + succ k = m via hk; succ_add transforms
 365    -- Wait: hk : n + succ k = m, and succ (n + k) = n + succ k by add_succ. So succ (n + k) = m.
 366    exact hk
 367  · rintro ⟨k, hk⟩
 368    refine ⟨k, ?_⟩