Proofgold Proof

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