feat(algebra/order): additional theorems on cmp

algebra/order.lean

@@ -216,4 +216,25 @@ theorem compares_of_strict_mono {β} [linear_order α] [preorder β]
 | eq := ⟨λ h, injective_of_strict_mono _ H h, congr_arg _⟩
 | gt := lt_iff_lt_of_strict_mono f H
 
+theorem swap_or_else (o₁ o₂) : (or_else o₁ o₂).swap = or_else o₁.swap o₂.swap :=
+by cases o₁; try {refl}; cases o₂; refl
+
+theorem or_else_eq_lt (o₁ o₂) : or_else o₁ o₂ = lt ↔ o₁ = lt ∨ (o₁ = eq ∧ o₂ = lt) :=
+by cases o₁; cases o₂; exact dec_trivial
+
 end ordering
+
+theorem cmp_compares [decidable_linear_order α] (a b : α) : (cmp a b).compares a b :=
+begin
+  unfold cmp cmp_using,
+  by_cases a < b; simp [h],
+  by_cases h₂ : b < a; simp [h₂, gt],
+  exact (lt_or_eq_of_le (le_of_not_gt h₂)).resolve_left h
+end
+
+theorem cmp_swap [preorder α] [@decidable_rel α (<)] (a b : α) : (cmp a b).swap = cmp b a :=
+begin
+  unfold cmp cmp_using,
+  by_cases a < b; by_cases h₂ : b < a; simp [h, h₂, gt, ordering.swap],
+  exact lt_asymm h h₂
+end

order/basic.lean

@@ -175,6 +175,13 @@ def linear_order.lift {α β} [linear_order β]
   (f : α → β) (inj : injective f) : linear_order α :=
 { le_total := λx y, le_total (f x) (f y), .. partial_order.lift f inj }
 
+def decidable_linear_order.lift {α β} [decidable_linear_order β]
+  (f : α → β) (inj : injective f) : decidable_linear_order α :=
+{ decidable_le := λ x y, show decidable (f x ≤ f y), by apply_instance,
+  decidable_lt := λ x y, show decidable (f x < f y), by apply_instance,
+  decidable_eq := λ x y, decidable_of_iff _ ⟨@inj x y, congr_arg f⟩,
+  .. linear_order.lift f inj }
+
 instance subtype.preorder {α} [preorder α] (p : α → Prop) : preorder (subtype p) :=
 preorder.lift subtype.val
 
@@ -423,4 +430,3 @@ theorem directed_mono {s : α → α → Prop} {ι} (f : ι → α)
 λ a b, let ⟨c, h₁, h₂⟩ := h a b in ⟨c, H _ _ h₁, H _ _ h₂⟩
 
 end
-