Proofgold Proof

pf
Apply nat_ordsucc_in_ordsucc with 13, 8 leaving 2 subgoals. The subproof is completed by applying nat_13. The subproof is completed by applying unknownprop_d21f00b59e27a2a5e30acb5e1bd89e8682be02902fa61c5da12efa36345aa0e9. ■