Proofgold Proof

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