Proofgold Proof

pf
Apply nat_ordsucc_in_ordsucc with 14, 13 leaving 2 subgoals. The subproof is completed by applying nat_14. The subproof is completed by applying unknownprop_331badb0bc2cb72fdd31f16934f9ba3896484f4038f5056bfa218c35501c067b. ■