Proofgold Proof

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