An exact proof term for the current goal is (nat_ordsucc 1 nat_1).