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