Proofgold Proof

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