Proofgold Proof

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