Let alpha be given.

Assume Ha.

Let beta be given.

Assume Hb.

Let gamma be given.

Assume Hc.

We prove the intermediate claim Lc: ordinal gamma.

An exact proof term for the current goal is ordinal_Hered alpha Ha gamma Hc.

We prove the intermediate claim Lab: ordinal (alpha + beta).

Apply add_SNo_ordinal_ordinal to the current goal.

An exact proof term for the current goal is Ha.

An exact proof term for the current goal is Hb.

We prove the intermediate claim Lcb: ordinal (gamma + beta).

Apply add_SNo_ordinal_ordinal to the current goal.

An exact proof term for the current goal is Lc.

An exact proof term for the current goal is Hb.

We will prove gamma + beta ∈ alpha + beta.

Apply ordinal_SNoLt_In (gamma + beta) (alpha + beta) Lcb Lab to the current goal.

We will prove gamma + beta < alpha + beta.

Apply add_SNo_Lt1 to the current goal.

Apply ordinal_SNo to the current goal.

An exact proof term for the current goal is Lc.

Apply ordinal_SNo to the current goal.

An exact proof term for the current goal is Hb.

Apply ordinal_SNo to the current goal.

An exact proof term for the current goal is Ha.

An exact proof term for the current goal is ordinal_In_SNoLt alpha Ha gamma Hc.

∎