Let x be given.

Assume Hx.

Let n be given.

Assume Hn.

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

∎