Proofgold Proof

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