Proofgold Proof

pf
Apply nat_ordsucc_in_ordsucc with 10, 9 leaving 2 subgoals. The subproof is completed by applying nat_10. The subproof is completed by applying unknownprop_83b7b73de92238880d97107189e7acf45f9dc154df0447f816815407ccfc32b3. ■