Proofgold Proof

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