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