no goals
α : Type ?u.49028
β : Type ?u.49031
K : Type u_1
inst✝ : DivisionRing K
a b c d : K
hab : _root_.Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)
simp only [inv_eq_one_div, (Commute.one_right a).div_sub_div hab ha hb, one_mul, mul_one]