lt

formal source

 325def le (n m : LogicNat) : Prop := ∃ k : LogicNat, n + k = m
 326
 327/-- Strict order on `LogicNat`. -/
 328def lt (n m : LogicNat) : Prop := ∃ k : LogicNat, n + succ k = m
 329
 330instance : LE LogicNat := ⟨le⟩
 331instance : LT LogicNat := ⟨lt⟩
 332
 333@[simp] theorem le_def (n m : LogicNat) : n ≤ m ↔ ∃ k, n + k = m := Iff.rfl
 334@[simp] theorem lt_def (n m : LogicNat) : n < m ↔ ∃ k, n + succ k = m := Iff.rfl
 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⟩