Proofgold Proof

pf
Apply nat_ordsucc_in_ordsucc with 10, 4 leaving 2 subgoals. The subproof is completed by applying nat_10. The subproof is completed by applying unknownprop_ba23a99d385c96fc20e18f31e2884f35e8c8dc96acf9973b3be03f8c1bfc0b50. ■