Proofgold Proof

pf
Apply nat_ordsucc_in_ordsucc with 11, 7 leaving 2 subgoals. The subproof is completed by applying nat_11. The subproof is completed by applying unknownprop_b18d702f5c2ec6e903ac736dc6097e920fbb275019c2bab4286a56feb5bf1ea2. ■