succ_le_succ

formal source

 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, ?_⟩
 369    show n + succ k = m
 370    rw [add_succ]
 371    show succ (n + k) = m
 372    rw [← succ_add]
 373    exact hk
 374
 375theorem lt_irrefl (n : LogicNat) : ¬ n < n := by
 376  rintro ⟨k, hk⟩
 377  -- n + succ k = n. Apply toNat: toNat n + toNat (succ k) = toNat n on Nat.
 378  have := congrArg toNat hk
 379  rw [toNat_add, toNat_succ] at this
 380  -- this : toNat n + Nat.succ (toNat k) = toNat n