Proofgold Proof

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