have tr' : a = b ∨ b < a ∨ a < b := by permutateOr tr, [1, 2, 0]
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a = b
tr : a < b ∨ a = b ∨ b < a
⊢ a < b
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a = b
tr : a < b ∨ a = b ∨ b < a
tr' : a = b ∨ b < a ∨ a < b
⊢ a < b