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

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