Proofgold Proof

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