have : sgn (p - q) ≄ 1 := by
  intro (_ : sgn (p - q) ≃ 1)
  show False
  have : p > q := gt_sgn.mpr ‹sgn (p - q) ≃ 1›
  have not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
    (order_trichotomy p q).atMostOne
  match ‹p < q ∨ p ≃ q› with
  | Or.inl (_ : p < q) =>
    have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
      AA.TwoOfThree.oneAndThree ‹p < q› ‹p > q›
    exact absurd two not_two
  | Or.inr (_ : p ≃ q) =>
    have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
      AA.TwoOfThree.twoAndThree ‹p ≃ q› ‹p > q›
    exact absurd two not_two
ℕ ℤ ℚ : 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 : ℚ
x✝ : p < q ∨ p ≃ q
⊢ p ≤ q
ℕ ℤ ℚ : 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 : ℚ
x✝ : p < q ∨ p ≃ q
this : sgn (p - q) ≄ 1
⊢ p ≤ q