Proofgold Proof

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