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