Proofgold Proof

pf
Apply unknownprop_ecf5eea45f41bf7adbe211aa6fc21085082149e5b6bd207afa72850cb193f7b3 with ordsucc, nat_p, 0 leaving 2 subgoals. The subproof is completed by applying nat_ordsucc. The subproof is completed by applying nat_0. ■