Proofgold Proof

pf
Apply nat_ordsucc_in_ordsucc with 12, 0 leaving 2 subgoals. The subproof is completed by applying nat_12. The subproof is completed by applying unknownprop_a2ef0c58cfd090f3c9e6e7916f6b56032d6bdd4de509aa9fb32f7308f99daf5a. ■