Proofgold Proof

pf
Apply add_nat_SR with u5, 0, λ x0 x1 . x1 = u6 leaving 2 subgoals. The subproof is completed by applying nat_0. Apply add_nat_0R with u5, λ x0 x1 . ordsucc x1 = u6. Let x0 of type ι → ι → ο be given. Assume H0: x0 (ordsucc u5) u6. The subproof is completed by applying H0. ■