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

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

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