Proofgold Proof

pf
Apply nat_ordsucc_in_ordsucc with 15, 0 leaving 2 subgoals. The subproof is completed by applying nat_15. The subproof is completed by applying unknownprop_524d83143154d5d95661710a112299dfd9761663d7039bc072fe66b06195afa1. ■