no goals
α : Type u_1
β : Type ?u.14282
K : Type ?u.14285
inst✝ : DivisionSemiring α
a b c d : α
hab : _root_.Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a + 1 / b = (a + b) / (a * b)
rw [(Commute.one_right a).div_add_div hab ha hb, one_mul, mul_one, add_comm]