Theorem: Smt.Reconstruct.Arith.trichotomy₁ (Smt/Reconstruct/Arith/Trichotomy/Lemmas.lean)

State before:
α : Type
inst✝ : LinearOrder α
a b : α
⊢ ¬a < b → ¬a = b → a > b
Tactic:
intros h₁ h₂
State after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
⊢ a > b

State before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
⊢ a > b
Tactic:
have tr := lt_trichotomy a b
State after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
tr : a < b ∨ a = b ∨ b < a
⊢ a > b

State before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
tr : a < b ∨ a = b ∨ b < a
⊢ a > b
Tactic:
exact (orImplies₃ ((orImplies₃ tr) h₁)) h₂
State after:
no goals