Proofgold Proof

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