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