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