Proofgold Proof

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