case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ False ↔ a ≥ b

case eq
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ True ↔ a ≥ b

case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ True ↔ a ≥ b
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b ≠ Ordering.lt ↔ a ≥ b
cases h : compare a b <;> simp only []
no goals
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ False ↔ a ≥ b
exact false_iff_iff.2 <| (lt_iff_not_ge a b).1 <| compare_lt_iff_lt.1 h
no goals
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ True ↔ a ≥ b
exact true_iff_iff.2 <| le_of_lt <| compare_gt_iff_gt.1 h