Proofgold Proof

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