Proofgold Proof

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