Theorem: IMOSL.IMO2013A5.good_injective (IMOSLLean4/IMO2013/A5/A5.lean)

State before:
f : ℕ → ℕ
h : good f
m n : ℕ
h0 : f^[4] m = f^[4] n
⊢ m = n
Tactic:
rwa [iter_four_eq h, iter_four_eq h n, add_right_inj] at h0
State after:
no goals