Proofgold Proof

pf
Apply unknownprop_5a55ae6da060bd3592cd2518e6392e5786971bf34a92b383078bce38ef6a8408 with ordsucc, nat_p, 9 leaving 2 subgoals. The subproof is completed by applying nat_ordsucc. The subproof is completed by applying nat_9. ■