English
Let q,r be rational numbers. Then the numerator of q − r, multiplied by q.den and r.den, satisfies (q − r).num · q.den · r.den = (q.num · r.den − r.num · q.den) · (q − r).den.
Русский
Пусть q,r — рациональные числа. Тогда при вычитании q − r выполняется равенство: числитель разности, умноженный на знаменатели q и r, равен разности поперечных произведений числителей, умноженной на знаменатель разности.
LaTeX
$$$(q - r).num \\cdot q.den \\cdot r.den = (q.num \\cdot r.den - r.num \\cdot q.den) \\cdot (q - r).den$$$
Lean4
theorem substr_num_den' (q r : ℚ) : (q - r).num * q.den * r.den = (q.num * r.den - r.num * q.den) * (q - r).den := by
rw [sub_eq_add_neg, sub_eq_add_neg, ← neg_mul, ← num_neg_eq_neg_num, ← den_neg_eq_den r, add_num_den' q (-r)]
