Proofgold Proof

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