Let alpha be given.

Assume Ha.

rewrite the current goal using add_SNo_0L alpha (ordinal_SNo alpha Ha) (from right to left) at position 1.

We will prove ordsucc (0 + alpha) = 1 + alpha.

Use symmetry.

An exact proof term for the current goal is add_SNo_ordinal_SL 0 ordinal_Empty alpha Ha.

∎