Let alpha be given.

Assume Ha: ordinal alpha.

Let beta be given.

Assume Hb: ordinal beta.

Let gamma be given.

Assume Hc: gamma ∈ 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 Lc: ordinal gamma.

An exact proof term for the current goal is ordinal_Hered beta Hb gamma Hc.

We prove the intermediate claim Lc2: SNo gamma.

An exact proof term for the current goal is ordinal_SNo gamma Lc.

rewrite the current goal using add_SNo_com alpha gamma La Lc2 (from left to right).

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

An exact proof term for the current goal is add_SNo_ordinal_InL beta Hb alpha Ha gamma Hc.

∎