no goals
α : Type u_1
β : Type ?u.8938
K : Type ?u.8941
inst✝ : DivisionSemiring α
a b c d : α
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)
rw [add_div, mul_div_mul_right _ b hd, hbc.eq, hbd.eq, mul_div_mul_right c d hb]