Theorem: IMOSL.IMO2014A4.map_map_zero_add (IMOSLLean4/IMO2014/A4/A4.lean)

State before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
y : ℤ
⊢ f (y + f 0) = c + f y
Tactic:
rw [← sub_eq_iff_eq_add, h, mul_zero, sub_self, zero_add]
State after:
no goals