Proofgold Proof

pf
Apply nat_ordsucc_in_ordsucc with 11, 10 leaving 2 subgoals. The subproof is completed by applying nat_11. The subproof is completed by applying unknownprop_ab3665aaa395ba5bc535a8f5a44f14a9771c7e237581e2ade81e4e145ecc82bc. ■