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