lt_iff_succ_le

formal source

 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
 381  omega
 382
 383theorem lt_trans {a b c : LogicNat} (hab : a < b) (hbc : b < c) : a < c := by
 384  rw [lt_iff_succ_le] at hab hbc ⊢
 385  exact le_trans hab (le_trans (le_succ b) hbc)
 386