Proofgold Proof

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