An exact proof term for the current goal is (nat_primrec_0 n (λ_ r ⇒ ordsucc r)).