have abs_ab : abs (a * b) ≤ ε * δ := calc
  _ ≃ abs (a * b)   := eqv_refl
  _ ≃ abs a * abs b := abs_compat_mul
  _ ≤ ε * abs b     := le_substL_mul_nonneg abs_nonneg ‹abs a ≤ ε›
  _ ≤ ε * δ         := le_substR_mul_nonneg ‹ε ≥ 0› ‹abs b ≤ δ›
ℕ ℤ ℚ : 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
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
this✝ : abs (a * r) ≤ ε * abs r
this : abs (p * b) ≤ δ * abs p
⊢ 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
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
this✝ : abs (a * r) ≤ ε * abs r
this : abs (p * b) ≤ δ * abs p
abs_ab : abs (a * b) ≤ ε * δ
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s