Proofgold Proof

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