@[simp]
theorem
Ordering.ite_eq_lt_distrib
(c : Prop)
[Decidable c]
(a b : Ordering)
:
((if c then a else b) = Ordering.lt) = if c then a = Ordering.lt else b = Ordering.lt
@[simp]
theorem
Ordering.ite_eq_eq_distrib
(c : Prop)
[Decidable c]
(a b : Ordering)
:
((if c then a else b) = Ordering.eq) = if c then a = Ordering.eq else b = Ordering.eq
@[simp]
theorem
Ordering.ite_eq_gt_distrib
(c : Prop)
[Decidable c]
(a b : Ordering)
:
((if c then a else b) = Ordering.gt) = if c then a = Ordering.gt else b = Ordering.gt
@[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]