Basic lemmas about comparing natural numbers

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

theorem 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

theorem 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

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