lt_irrefl

formal source

 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
 387theorem zero_lt_succ (n : LogicNat) : zero < succ n :=
 388  ⟨n, by show zero + succ n = succ n; rw [zero_add]⟩
 389
 390theorem lt_iff_le_and_ne {a b : LogicNat} : a < b ↔ a ≤ b ∧ a ≠ b := by
 391  constructor
 392  · rintro ⟨k, hk⟩
 393    refine ⟨⟨succ k, hk⟩, ?_⟩
 394    intro hab
 395    rw [hab] at hk
 396    -- b + succ k = b means succ k = 0 by additive cancellation; impossible.
 397    have := congrArg toNat hk
 398    rw [toNat_add, toNat_succ] at this
 399    omega
 400  · rintro ⟨⟨k, hk⟩, hne⟩
 401    -- a + k = b, a ≠ b, so k ≠ 0; k = succ k' for some k'.
 402    cases k with
 403    | identity =>
 404      exfalso
 405      apply hne