Let α be given.
Assume Ha: ordinal α.
Apply ordinal_ind to the current goal.
Let β be given.
Assume Hb: ordinal β.
Assume IH: ∀δ ∈ β, ordsucc α + δ = ordsucc (α + δ).
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 Lab: ordinal (α + β).
An exact proof term for the current goal is add_SNo_ordinal_ordinal α Ha β Hb.
We prove the intermediate claim LSa: ordinal (ordsucc α).
Apply ordinal_ordsucc to the current goal.
An exact proof term for the current goal is Ha.
We prove the intermediate claim LSa2: SNo (ordsucc α).
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is LSa.
We prove the intermediate claim LSab: ordinal (ordsucc α + β).
An exact proof term for the current goal is add_SNo_ordinal_ordinal (ordsucc α) LSa β Hb.
Set Lo1 to be the term {x + β|x ∈ SNoS_ (ordsucc α)}.
Set Lo2 to be the term {ordsucc α + x|x ∈ SNoS_ β}.
Apply SNoCutP_SNoCut (Lo1 ∪ Lo2) Empty (add_SNo_ordinal_SNoCutP (ordsucc α) LSa β Hb) to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume _.
rewrite the current goal using add_SNo_ordinal_eq (ordsucc α) LSa β Hb (from right to left).
Assume H1: ∀x ∈ Lo1 ∪ Lo2, x < ordsucc α + β.
Assume _.
Assume H2: ∀z, SNo z → (∀x ∈ Lo1 ∪ Lo2, x < z) → (∀y ∈ Empty, z < y) → SNoLev (ordsucc α + β) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (ordsucc α + β)) (ordsucc α + β) z.
We prove the intermediate claim L1: α + β ∈ ordsucc α + β.
Apply ordinal_SNoLt_In (α + β) (ordsucc α + β) Lab LSab to the current goal.
We will prove α + β < ordsucc α + β.
Apply H1 to the current goal.
We will prove α + β ∈ Lo1 ∪ Lo2.
Apply binunionI1 to the current goal.
We will prove α + β ∈ {x + β|x ∈ SNoS_ (ordsucc α)}.
Apply ReplI (SNoS_ (ordsucc α)) (λx ⇒ x + β) α to the current goal.
We will prove α ∈ SNoS_ (ordsucc α).
Apply SNoS_I (ordsucc α) LSa α α (ordsuccI2 α) to the current goal.
We will prove SNo_ α α.
An exact proof term for the current goal is ordinal_SNo_ α Ha.
Apply ordinal_ordsucc_In_eq (ordsucc α + β) (α + β) LSab L1 to the current goal.
Assume H3: ordsucc (α + β) ∈ ordsucc α + β.
We will prove False.
Set z to be the term ordsucc (α + β).
We prove the intermediate claim Lz: ordinal z.
An exact proof term for the current goal is ordinal_ordsucc (α + β) Lab.
We prove the intermediate claim Lz1: TransSet z.
An exact proof term for the current goal is ordinal_TransSet z Lz.
We prove the intermediate claim Lz2: SNo z.
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is Lz.
We prove the intermediate claim L2: SNoLev (ordsucc α + β) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (ordsucc α + β)) (ordsucc α + β) z.
Apply H2 z (ordinal_SNo z Lz) to the current goal.
Let w be given.
Assume Hw: w ∈ Lo1 ∪ Lo2.
We will prove w < z.
Apply binunionE Lo1 Lo2 w Hw to the current goal.
Assume H4: w ∈ Lo1.
Apply ReplE_impred (SNoS_ (ordsucc α)) (λx ⇒ x + β) w H4 to the current goal.
Let x be given.
Assume Hx: x ∈ SNoS_ (ordsucc α).
Assume Hwx: w = x + β.
Apply SNoS_E2 (ordsucc α) LSa x Hx to the current goal.
Assume Hx1: SNoLev x ∈ ordsucc α.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
We will prove w < z.
rewrite the current goal using Hwx (from left to right).
We will prove x + β < z.
We prove the intermediate claim LLxb: ordinal (SNoLev x + β).
An exact proof term for the current goal is add_SNo_ordinal_ordinal (SNoLev x) Hx2 β Hb.
We prove the intermediate claim LLxb2: SNo (SNoLev x + β).
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is LLxb.
Apply SNoLeLt_tra (x + β) (SNoLev x + β) z (SNo_add_SNo x β Hx3 Lb) LLxb2 Lz2 to the current goal.
We will prove x + β ≤ SNoLev x + β.
Apply add_SNo_Le1 x β (SNoLev x) Hx3 Lb (ordinal_SNo (SNoLev x) Hx2) to the current goal.
We will prove x ≤ SNoLev x.
An exact proof term for the current goal is ordinal_SNoLev_max_2 (SNoLev x) Hx2 x Hx3 (ordsuccI2 (SNoLev x)).
We will prove SNoLev x + β < z.
Apply SNoLeLt_tra (SNoLev x + β) (α + β) z LLxb2 (ordinal_SNo (α + β) Lab) Lz2 to the current goal.
We will prove SNoLev x + β ≤ α + β.
Apply add_SNo_Le1 (SNoLev x) β α (ordinal_SNo (SNoLev x) Hx2) Lb La to the current goal.
We will prove SNoLev x ≤ α.
Apply ordinal_Subq_SNoLe (SNoLev x) α Hx2 Ha to the current goal.
We will prove SNoLev x ⊆ α.
Apply ordsuccE α (SNoLev x) Hx1 to the current goal.
Assume H5: SNoLev x ∈ α.
Apply Ha to the current goal.
Assume Ha1 _.
An exact proof term for the current goal is Ha1 (SNoLev x) H5.
Assume H5: SNoLev x = α.
rewrite the current goal using H5 (from left to right).
Apply Subq_ref to the current goal.
We will prove α + β < z.
An exact proof term for the current goal is ordinal_In_SNoLt z Lz (α + β) (ordsuccI2 (α + β)).
Assume H4: w ∈ Lo2.
Apply ReplE_impred (SNoS_ β) (λx ⇒ ordsucc α + x) w H4 to the current goal.
Let x be given.
Assume Hx: x ∈ SNoS_ β.
Assume Hwx: w = ordsucc α + x.
Apply SNoS_E2 β Hb x Hx to the current goal.
Assume Hx1: SNoLev x ∈ β.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
We will prove w < z.
rewrite the current goal using Hwx (from left to right).
We will prove ordsucc α + x < z.
We prove the intermediate claim IHLx: ordsucc α + SNoLev x = ordsucc (α + SNoLev x).
An exact proof term for the current goal is IH (SNoLev x) Hx1.
We prove the intermediate claim LSax: SNo (ordsucc α + x).
An exact proof term for the current goal is SNo_add_SNo (ordsucc α) x LSa2 Hx3.
We prove the intermediate claim LaLx: ordinal (α + SNoLev x).
An exact proof term for the current goal is add_SNo_ordinal_ordinal α Ha (SNoLev x) Hx2.
We prove the intermediate claim LSaLx: ordinal (ordsucc α + SNoLev x).
An exact proof term for the current goal is add_SNo_ordinal_ordinal (ordsucc α) LSa (SNoLev x) Hx2.
We prove the intermediate claim LSaLx2: SNo (ordsucc α + SNoLev x).
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is LSaLx.
Apply SNoLeLt_tra (ordsucc α + x) (ordsucc α + SNoLev x) z LSax LSaLx2 Lz2 to the current goal.
We will prove ordsucc α + x ≤ ordsucc α + SNoLev x.
Apply add_SNo_Le2 (ordsucc α) x (SNoLev x) LSa2 Hx3 (ordinal_SNo (SNoLev x) Hx2) to the current goal.
We will prove x ≤ SNoLev x.
An exact proof term for the current goal is ordinal_SNoLev_max_2 (SNoLev x) Hx2 x Hx3 (ordsuccI2 (SNoLev x)).
We will prove ordsucc α + SNoLev x < z.
rewrite the current goal using IHLx (from left to right).
We will prove ordsucc (α + SNoLev x) < ordsucc (α + β).
Apply ordinal_In_SNoLt z Lz (ordsucc (α + SNoLev x)) to the current goal.
We will prove ordsucc (α + SNoLev x) ∈ ordsucc (α + β).
Apply ordinal_ordsucc_In (α + β) Lab to the current goal.
We will prove α + SNoLev x ∈ α + β.
Apply ordinal_SNoLt_In (α + SNoLev x) (α + β) LaLx Lab to the current goal.
We will prove α + SNoLev x < α + β.
Apply add_SNo_Lt2 α (SNoLev x) β La (ordinal_SNo (SNoLev x) Hx2) Lb to the current goal.
We will prove SNoLev x < β.
Apply ordinal_In_SNoLt β Hb (SNoLev x) to the current goal.
We will prove SNoLev x ∈ β.
An exact proof term for the current goal is Hx1.
Let w be given.
Assume Hw: w ∈ Empty.
We will prove False.
An exact proof term for the current goal is EmptyE w Hw.
Apply L2 to the current goal.
rewrite the current goal using ordinal_SNoLev (ordsucc α + β) LSab (from left to right).
rewrite the current goal using ordinal_SNoLev z Lz (from left to right).
Assume H4: ordsucc α + β ⊆ z.
Assume _.
Apply In_irref z to the current goal.
Apply H4 to the current goal.
We will prove z ∈ ordsucc α + β.
An exact proof term for the current goal is H3.
Assume H3: ordsucc α + β = ordsucc (α + β).
An exact proof term for the current goal is H3.
∎