have : min p q ≃ min q p := calc
  _ ≃ min p q := eqv_refl
  _ ≃ q       := ‹min p q ≃ q›
  _ ≃ min q p := eqv_symm ‹min 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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ q
⊢ Ordered.min p q ≃ Ordered.min 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.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ q
this : Ordered.min p q ≃ Ordered.min q p
⊢ Ordered.min p q ≃ Ordered.min q p