Let α be given.

Assume Ha.

Let β be given.

Assume Hb.

Let γ be given.

Assume Hc.

We prove the intermediate claim Lc: ordinal γ.

An exact proof term for the current goal is ordinal_Hered α Ha γ Hc.

We prove the intermediate claim Lab: ordinal (α + β).

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 (γ + β).

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 γ + β ∈ α + β.

Apply ordinal_SNoLt_In (γ + β) (α + β) Lcb Lab to the current goal.

We will prove γ + β < α + β.

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 α Ha γ Hc.

∎