case mp =>
  intro (_ : p ≤ q)
  show p < q ∨ p ≃ q
  have : AA.OneOfThree (p < q) (p ≃ q) (p > q) :=
    (order_trichotomy p q).atLeastOne
  match this with
  | AA.OneOfThree.first (_ : p < q) =>
    have : p < q ∨ p ≃ q := Or.inl ‹p < q›
    exact this
  | AA.OneOfThree.second (_ : p ≃ q) =>
    have : p < q ∨ p ≃ q := Or.inr ‹p ≃ q›
    exact this
  | AA.OneOfThree.third (_ : p > q) =>
    have : sgn (p - q) ≃ 1 := gt_sgn.mp ‹p > q›
    have : sgn (p - q) ≄ 1 := le_sgn.mp ‹p ≤ q›
    exact absurd ‹sgn (p - q) ≃ 1› ‹sgn (p - q) ≄ 1›
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≤ q → p < q ∨ p ≃ q
no goals