Let alpha be given.
Assume Ha: ordinal alpha.
Let beta be given.
Assume Hb: ordinal 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 Lab1: SNo (alpha + beta).
An exact proof term for the current goal is SNo_add_SNo alpha beta La Lb.
We prove the intermediate claim Lab2: ordinal (SNoLev (alpha + beta)).
An exact proof term for the current goal is SNoLev_ordinal (alpha + beta) Lab1.
We will prove ordinal (alpha + beta).
Apply SNo_max_ordinal (alpha + beta) Lab1 to the current goal.
We will prove ∀y ∈ SNoS_ (SNoLev (alpha + beta)), y < alpha + beta.
Let y be given.
Assume Hy: y ∈ SNoS_ (SNoLev (alpha + beta)).
Apply SNoS_E2 (SNoLev (alpha + beta)) Lab2 y Hy to the current goal.
Assume Hy1: SNoLev y ∈ SNoLev (alpha + beta).
Assume Hy2: ordinal (SNoLev y).
Assume Hy3: SNo y.
Assume Hy4: SNo_ (SNoLev y) y.
Set Lo1 to be the term {x + beta|x ∈ SNoS_ alpha}.
Set Lo2 to be the term {alpha + x|x ∈ SNoS_ beta}.
Apply SNoLt_trichotomy_or y (alpha + beta) Hy3 Lab1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: y < alpha + beta.
An exact proof term for the current goal is H1.
Assume H1: y = alpha + beta.
We will prove False.
Apply In_irref (SNoLev y) to the current goal.
rewrite the current goal using H1 (from left to right) at position 2.
An exact proof term for the current goal is Hy1.
Assume H1: alpha + beta < y.
We will prove False.
Apply add_SNo_ordinal_SNoCutP alpha Ha beta Hb to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: ∀x ∈ Lo1 ∪ Lo2, SNo x.
Assume _ _.
Apply SNoCutP_SNoCut (Lo1 ∪ Lo2) Empty (add_SNo_ordinal_SNoCutP alpha Ha beta Hb) to the current goal.
Assume H3.
Apply H3 to the current goal.
Assume H3.
Apply H3 to the current goal.
Assume _.
Assume H3: ∀x ∈ Lo1 ∪ Lo2, x < SNoCut (Lo1 ∪ Lo2) Empty.
Assume _.
Assume H4: ∀z, SNo z → (∀x ∈ Lo1 ∪ Lo2, x < z) → (∀y ∈ Empty, z < y) → SNoLev (SNoCut (Lo1 ∪ Lo2) Empty) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut (Lo1 ∪ Lo2) Empty)) (SNoCut (Lo1 ∪ Lo2) Empty) z.
We prove the intermediate claim L1: SNoLev (alpha + beta) ⊆ SNoLev y ∧ SNoEq_ (SNoLev (alpha + beta)) (alpha + beta) y.
rewrite the current goal using add_SNo_ordinal_eq alpha Ha beta Hb (from left to right).
Apply H4 y Hy3 to the current goal.
Let w be given.
Assume Hw: w ∈ Lo1 ∪ Lo2.
We will prove w < y.
Apply SNoLt_tra w (alpha + beta) y (H2 w Hw) Lab1 Hy3 to the current goal.
We will prove w < alpha + beta.
rewrite the current goal using add_SNo_ordinal_eq alpha Ha beta Hb (from left to right).
An exact proof term for the current goal is H3 w Hw.
We will prove alpha + beta < y.
An exact proof term for the current goal is H1.
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 L1 to the current goal.
Assume H5: SNoLev (alpha + beta) ⊆ SNoLev y.
Assume _.
Apply In_irref (SNoLev y) to the current goal.
Apply H5 to the current goal.
An exact proof term for the current goal is Hy1.
∎