no goals
α : Type ?u.10115
β : Type ?u.10118
o₁ o₂ : Ordering
⊢ orElse o₁ o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt
cases o₁ <;> cases o₂ <;> exact by decide
no goals
α : Type ?u.10115
β : Type ?u.10118
⊢ orElse gt gt = lt ↔ gt = lt ∨ gt = eq ∧ gt = lt
decide