Proofgold Proof

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