Theorem: IMOSL.IMO2011A4.PNat_eq_Nat_conj_iff (IMOSLLean4/IMO2011/A4/A4.lean)

State before:
f : ℕ+ → ℕ+
g : ℕ → ℕ
h : g = fun n => (f n.succPNat).natPred
n : ℕ+
⊢ f n = (g n.natPred).succPNat
Tactic:
rw [h, PNat.succPNat_natPred, PNat.succPNat_natPred]
State after:
no goals