Proofgold Proof

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