Proofgold Proof

pf
Apply nat_ordsucc_in_ordsucc with 14, 8 leaving 2 subgoals. The subproof is completed by applying nat_14. The subproof is completed by applying unknownprop_f2e483493aff88182c91ba90344f3fdfdd75e2acab769b9d50a99359063f03f5. ■