Let f and n be given.

Assume Hn.

We will prove Pi_nat f (ordsucc n) = Pi_nat f n * f n.

An exact proof term for the current goal is nat_primrec_S 1 (λi r ⇒ r * f i) n Hn.

∎