Theorem: Imo2017P2.good_shift2 (Compfiles/Imo2017P2.lean)

State before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
x : D
⊢ f (x - 1) = f x + 1
Tactic:
rw [← good_shift h h0, sub_add_cancel]
State after:
no goals