have : s - r ≃ b := calc
  _ ≃ s - r        := eqv_refl
  _ ≃ s + -r       := sub_add_neg
  _ ≃ -r + s       := add_comm
  _ ≃ -r + (r + b) := add_substR ‹s ≃ r + b›
  _ ≃ (-r + r) + b := eqv_symm add_assoc
  _ ≃ 0 + b        := add_substL add_inverseL
  _ ≃ b            := add_identL
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
ε δ p q r s : ℚ
x✝¹ : p ⊢ε⊣ q
x✝ : r ⊢δ⊣ s
close_diff : ∀ {x y ζ : ℚ}, x ⊢ζ⊣ y → ∃ d, y ≃ x + d ∧ abs d ≤ ζ
a : ℚ
left✝¹ : q ≃ p + a
right✝¹ : abs a ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this : ε ≥ 0
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
ε δ p q r s : ℚ
x✝¹ : p ⊢ε⊣ q
x✝ : r ⊢δ⊣ s
close_diff : ∀ {x y ζ : ℚ}, x ⊢ζ⊣ y → ∃ d, y ≃ x + d ∧ abs d ≤ ζ
a : ℚ
left✝¹ : q ≃ p + a
right✝¹ : abs a ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝ : ε ≥ 0
this : s - r ≃ b
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s