no goals
α : Type ?u.40731
β : Type ?u.40734
K : Type u_1
inst✝ : DivisionRing K
a✝ b✝ c d a b : K
h : b ≠ 0
⊢ (a - b) / b = a / b - 1
simpa only [← @div_self _ _ b h] using (div_sub_div_same a b b).symm