Proofgold Proof

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