have opposite_eqv
    {r s x y : ℚ} : max r s ≃ x → max s r ≃ y → y ≤ max r s → x ≤ max s r →
    max r s ≃ max s r
    := by
  intro (_ : max r s ≃ x) (_ : max s r ≃ y)
  intro (_ : y ≤ max r s) (_ : x ≤ max s r)
  show max r s ≃ max s r
  have : y ≤ x := le_substR_eqv ‹max r s ≃ x› ‹y ≤ max r s›
  have : x ≤ y := le_substR_eqv ‹max s r ≃ y› ‹x ≤ max s r›
  have : x ≃ y := le_antisymm ‹x ≤ y› ‹y ≤ x›
  have : max r s ≃ max s r := calc
    _ ≃ max r s := eqv_refl
    _ ≃ x       := ‹max r s ≃ x›
    _ ≃ y       := ‹x ≃ y›
    _ ≃ max s r := eqv_symm ‹max s r ≃ y›
  exact this
ℕ ℤ ℚ : 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 : ℚ
⊢ 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
⊢ Ordered.max p q ≃ Ordered.max q p