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