@[simp]
theorem
ordering.ite_eq_lt_distrib
(c : Prop)
[decidable c]
(a b : ordering) :
ite c a b = ordering.lt = ite c (a = ordering.lt) (b = ordering.lt)
@[simp]
theorem
ordering.ite_eq_eq_distrib
(c : Prop)
[decidable c]
(a b : ordering) :
ite c a b = ordering.eq = ite c (a = ordering.eq) (b = ordering.eq)
@[simp]
theorem
ordering.ite_eq_gt_distrib
(c : Prop)
[decidable c]
(a b : ordering) :
ite c a b = ordering.gt = ite c (a = ordering.gt) (b = ordering.gt)
@[simp]
theorem
cmp_using_eq_lt
{α : Type u}
{lt : α → α → Prop}
[decidable_rel lt]
(a b : α) :
cmp_using lt a b = ordering.lt = lt a b
@[simp]
theorem
cmp_using_eq_gt
{α : Type u}
{lt : α → α → Prop}
[decidable_rel lt]
[is_strict_order α lt]
(a b : α) :
cmp_using lt a b = ordering.gt = lt b a
@[simp]