Proofgold Proof

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