An exact proof term for the current goal is nat_ordsucc 3 nat_3.