Let α be given.

Assume Ha: ordinal α.

Let β be given.

Assume Hb: ordinal β.

We prove the intermediate claim La: SNo α.

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

We prove the intermediate claim Lb: SNo β.

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

We prove the intermediate claim La: SNo α.

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

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

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 β).

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

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

We will prove ordsucc β + α = ordsucc (α + β).

rewrite the current goal using add_SNo_ordinal_SL β Hb α Ha (from left to right).

We will prove ordsucc (β + α) = ordsucc (α + β).

rewrite the current goal using add_SNo_com β α Lb La (from left to right).

Use reflexivity.

∎