Some Ordering lemmas

@[simp]

theorem Ordering.ite_eq_lt_distrib (c : Prop) [Decidable c] (a b : Ordering) : ((if c then a else b) = lt) = if c then a = lt else b = lt

@[simp]

theorem Ordering.ite_eq_eq_distrib (c : Prop) [Decidable c] (a b : Ordering) : ((if c then a else b) = eq) = if c then a = eq else b = eq

@[simp]

theorem Ordering.ite_eq_gt_distrib (c : Prop) [Decidable c] (a b : Ordering) : ((if c then a else b) = gt) = if c then a = gt else b = gt

@[simp]

theorem Ordering.dthen_eq_then (o₁ o₂ : Ordering) : (o₁.dthen fun (x : o₁ = eq) => o₂) = o₁.then o₂

@[simp]

theorem cmpUsing_eq_lt {α : Type u} {lt : α → α → Prop} [DecidableRel lt] (a b : α) : (cmpUsing lt a b = Ordering.lt) = lt a b

@[simp]

theorem cmpUsing_eq_gt {α : Type u} {lt : α → α → Prop} [DecidableRel lt] [IsStrictOrder α lt] (a b : α) : cmpUsing lt a b = Ordering.gt ↔ lt b a

@[simp]

theorem cmpUsing_eq_eq {α : Type u} {lt : α → α → Prop} [DecidableRel lt] (a b : α) : cmpUsing lt a b = Ordering.eq ↔ ¬lt a b ∧ ¬lt b a