Basic lemmas about comparing natural numbers

This file introduce some basic lemmas about compare as applied to natural numbers.

Import Std.Classes.Ord in order to obtain the TransOrd and LawfulEqOrd instances for Nat.

theorem Nat.compare_eq_ite_lt (a b : Nat) : compare a b = if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq

@[deprecated Nat.compare_eq_ite_lt (since := "2025-03_28")]

def Nat.compare_def_lt (a b : Nat) : compare a b = if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq

Equations

• Nat.compare_def_lt = Nat.compare_eq_ite_lt

theorem Nat.compare_eq_ite_le (a b : Nat) : compare a b = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

@[deprecated Nat.compare_eq_ite_le (since := "2025-03_28")]

def Nat.compare_def_le (a b : Nat) : compare a b = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

Equations

• Nat.compare_def_le = Nat.compare_eq_ite_le

theorem Nat.compare_swap (a b : Nat) : (compare a b).swap = compare b a

theorem Nat.compare_eq_eq {a b : Nat} : compare a b = Ordering.eq ↔ a = b

theorem Nat.compare_eq_lt {a b : Nat} : compare a b = Ordering.lt ↔ a < b

theorem Nat.compare_eq_gt {a b : Nat} : compare a b = Ordering.gt ↔ b < a

theorem Nat.compare_ne_gt {a b : Nat} : compare a b ≠ Ordering.gt ↔ a ≤ b

theorem Nat.compare_ne_lt {a b : Nat} : compare a b ≠ Ordering.lt ↔ b ≤ a

theorem Nat.isLE_compare {a b : Nat} : (compare a b).isLE = true ↔ a ≤ b

theorem Nat.isGE_compare {a b : Nat} : (compare a b).isGE = true ↔ b ≤ a