Proofgold Proof

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