An exact proof term for the current goal is (nat_ordsucc 0 nat_0).