Proofgold Proof

pf
Apply nat_ordsucc_in_ordsucc with 13, 12 leaving 2 subgoals. The subproof is completed by applying nat_13. The subproof is completed by applying unknownprop_aac233feaa0aa18324c0d692b3f19bd8318b55545ab88208c741a1f8b442a053. ■