have : q ≤ max p q := max_leR
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ p
h✝ : Ordered.max q p ≃ q
⊢ Ordered.max p q ≃ Ordered.max q p
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.max r s ≃ x →
      Ordered.max s r ≃ y → y ≤ Ordered.max r s → x ≤ Ordered.max s r → Ordered.max r s ≃ Ordered.max s r
pq_cases : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
qp_cases : Ordered.max q p ≃ q ∨ Ordered.max q p ≃ p
h✝¹ : Ordered.max p q ≃ p
h✝ : Ordered.max q p ≃ q
this : q ≤ Ordered.max p q
⊢ Ordered.max p q ≃ Ordered.max q p