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