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