Let n and m be given.

Assume Hm.

We will prove nat_primrec 1 (λ_ r ⇒ n * r) (ordsucc m) = n * nat_primrec 1 (λ_ r ⇒ n * r) m.

An exact proof term for the current goal is nat_primrec_S 1 (λ_ r ⇒ n * r) m Hm.

∎