Proofgold Proof

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