Let α be given.

Assume Ha.

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

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

Use symmetry.

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

∎