Let alpha be given.

Assume Ha: ordinal alpha.

Let beta be given.

Assume Hb: ordinal beta.

We prove the intermediate claim La: SNo alpha.

An exact proof term for the current goal is ordinal_SNo alpha Ha.

We prove the intermediate claim Lb: SNo beta.

An exact proof term for the current goal is ordinal_SNo beta Hb.

We prove the intermediate claim La: SNo alpha.

An exact proof term for the current goal is ordinal_SNo alpha Ha.

We prove the intermediate claim LSb: ordinal (ordsucc beta).

Apply ordinal_ordsucc to the current goal.

An exact proof term for the current goal is Hb.

We prove the intermediate claim LSb2: SNo (ordsucc beta).

An exact proof term for the current goal is ordinal_SNo (ordsucc beta) LSb.

rewrite the current goal using add_SNo_com alpha (ordsucc beta) La LSb2 (from left to right).

We will prove ordsucc beta + alpha = ordsucc (alpha + beta).

rewrite the current goal using add_SNo_ordinal_SL beta Hb alpha Ha (from left to right).

We will prove ordsucc (beta + alpha) = ordsucc (alpha + beta).

rewrite the current goal using add_SNo_com beta alpha Lb La (from left to right).

Use reflexivity.

∎