Basic lemmas about comparing integers

This file introduces some basic lemmas about compare as applied to integers.

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

theorem Int.lt_or_eq_of_le {n m : Int} (h : n ≤ m) : n < m ∨ n = m

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

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

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

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

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

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

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

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

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

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