Proofgold Proof

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