Proofgold Proof

pf
Apply nat_ordsucc_in_ordsucc with 13, 7 leaving 2 subgoals. The subproof is completed by applying nat_13. The subproof is completed by applying unknownprop_269184d50a39177d43eb370da2d073bdeface4a938fbbb03dcf5be3dc6e07dc8. ■