Proofgold Proof

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