Proofgold Proof

pf
Apply nat_ordsucc_in_ordsucc with 15, 12 leaving 2 subgoals. The subproof is completed by applying nat_15. The subproof is completed by applying unknownprop_aa483142be20403c05651093e77bf2da9ed1089804c07ed444e477459b766dab. ■