have qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b := calc
  _ ≃ q * s - p * r                := eqv_refl
  _ ≃ (p + a) * s - p * r          := sub_substL (mul_substL ‹q ≃ p + a›)
  _ ≃ p * s + a * s - p * r        := sub_substL mul_distribR
  _ ≃ p * s + a * s + (-(p * r))   := sub_add_neg
  _ ≃ p * s + (a * s + (-(p * r))) := add_assoc
  _ ≃ p * s + (-(p * r) + a * s)   := add_substR add_comm
  _ ≃ p * s + (-(p * r)) + a * s   := eqv_symm add_assoc
  _ ≃ p * s - p * r + a * s        := add_substL (eqv_symm sub_add_neg)
  _ ≃ p * (s - r) + a * s          := add_substL (eqv_symm mul_distribL_sub)
  _ ≃ p * b + a * s                := add_substL (mul_substR ‹s - r ≃ b›)
  _ ≃ p * b + a * (r + b)          := add_substR (mul_substR ‹s ≃ r + b›)
  _ ≃ p * b + (a * r + a * b)      := add_substR mul_distribL
  _ ≃ p * b + a * r + a * b        := eqv_symm add_assoc
ℕ ℤ ℚ : 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
ℕ ℤ ℚ : 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
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s