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