no goals
α : Type ?u.42064
β : Type ?u.42067
K : Type u_1
inst✝ : DivisionRing K
a✝ b✝ c d a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = a⁻¹ * (b - a) * b⁻¹
rw [mul_sub, sub_mul, mul_inv_cancel_right₀ hb, inv_mul_cancel ha, one_mul]