Proofgold Proof

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