Proofgold Proof

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