Proofgold Proof

pf
Apply nat_ordsucc_in_ordsucc with 12, 5 leaving 2 subgoals. The subproof is completed by applying nat_12. The subproof is completed by applying unknownprop_75d836f404cbbeae78f524a2ea7f26282023039d9accd25589aa1c1720bb8121. ■