no goals
α : Type ?u.44091
β : Type ?u.44094
K : Type u_1
inst✝ : DivisionRing K
a b c d : K
hbc : _root_.Commute b c
hbd : _root_.Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b - c / d = (a * d - b * c) / (b * d)
simpa only [mul_neg, neg_div, ← sub_eq_add_neg] using hbc.neg_right.div_add_div hbd hb hd