lt_iff_le_and_ne

formal source

 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
 406      simpa using hk
 407    | step k' => exact ⟨k', hk⟩
 408
 409theorem le_antisymm {a b : LogicNat} (hab : a ≤ b) (hba : b ≤ a) : a = b := by
 410  obtain ⟨k1, hk1⟩ := hab
 411  obtain ⟨k2, hk2⟩ := hba
 412  have h1 := congrArg toNat hk1
 413  have h2 := congrArg toNat hk2
 414  rw [toNat_add] at h1 h2
 415  -- toNat a + toNat k1 = toNat b, toNat b + toNat k2 = toNat a.
 416  have hnat : toNat a = toNat b := by omega
 417  -- Lift to LogicNat via the equivalence.
 418  have := congrArg fromNat hnat
 419  rw [fromNat_toNat, fromNat_toNat] at this
 420  exact this