Proofgold Proof

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