Apply SNoLev_ind to the current goal.

Let u be given.

Assume Hu1: SNo u.

Assume IH: ∀z ∈ SNoS_ (SNoLev u), SNoLev z ∈ SNoLev (x + y) → z < x + y → (∃v ∈ SNoL x, z ≤ v + y) ∨ (∃v ∈ SNoL y, z ≤ x + v).

Assume Hu2: SNoLev u ∈ SNoLev (x + y).

Assume Hu3: u < x + y.

Apply dneg to the current goal.

Assume HNC: ¬ ((∃v ∈ SNoL x, u ≤ v + y) ∨ (∃v ∈ SNoL y, u ≤ x + v)).

Apply SNoLt_irref u to the current goal.

We will prove u < u.

Apply SNoLtLe_tra u (x + y) u Hu1 Lxy Hu1 Hu3 to the current goal.

We will prove x + y ≤ u.

Set Lxy1 to be the term {w + y|w ∈ SNoL x}.

Set Lxy2 to be the term {x + w|w ∈ SNoL y}.

Set Rxy1 to be the term {z + y|z ∈ SNoR x}.

Set Rxy2 to be the term {x + z|z ∈ SNoR y}.

rewrite the current goal using add_SNo_eq x Hx y Hy (from left to right).

We will prove SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2) ≤ u.

rewrite the current goal using SNo_eta u Hu1 (from left to right).

We will prove SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2) ≤ SNoCut (SNoL u) (SNoR u).

Apply SNoCut_Le (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2) (SNoL u) (SNoR u) to the current goal.

An exact proof term for the current goal is add_SNo_SNoCutP x y Hx Hy.

An exact proof term for the current goal is SNoCutP_SNoL_SNoR u Hu1.

rewrite the current goal using SNo_eta u Hu1 (from right to left).

We will prove ∀w ∈ Lxy1 ∪ Lxy2, w < u.

Let w be given.

Assume Hw: w ∈ Lxy1 ∪ Lxy2.

Apply binunionE Lxy1 Lxy2 w Hw to the current goal.

Assume Hw2: w ∈ Lxy1.

We will prove w < u.

Apply ReplE_impred (SNoL x) (λw ⇒ w + y) w Hw2 to the current goal.

Let v be given.

Assume Hv: v ∈ SNoL x.

Assume Hwv: w = v + y.

Apply SNoL_E x Hx v Hv to the current goal.

Assume Hv1: SNo v.

Assume Hv2: SNoLev v ∈ SNoLev x.

Assume Hv3: v < x.

rewrite the current goal using Hwv (from left to right).

We will prove v + y < u.

We prove the intermediate claim Lvy: SNo (v + y).

An exact proof term for the current goal is SNo_add_SNo v y Hv1 Hy.

Apply SNoLtLe_or (v + y) u Lvy Hu1 to the current goal.

Assume H1: v + y < u.

An exact proof term for the current goal is H1.

Assume H1: u ≤ v + y.

We will prove False.

Apply HNC to the current goal.

Apply orIL to the current goal.

We use v to witness the existential quantifier.

Apply andI to the current goal.

We will prove v ∈ SNoL x.

An exact proof term for the current goal is Hv.

We will prove u ≤ v + y.

An exact proof term for the current goal is H1.

Assume Hw2: w ∈ Lxy2.

We will prove w < u.

Apply ReplE_impred (SNoL y) (λw ⇒ x + w) w Hw2 to the current goal.

Let v be given.

Assume Hv: v ∈ SNoL y.

Assume Hwv: w = x + v.

Apply SNoL_E y Hy v Hv to the current goal.

Assume Hv1: SNo v.

Assume Hv2: SNoLev v ∈ SNoLev y.

Assume Hv3: v < y.

rewrite the current goal using Hwv (from left to right).

We will prove x + v < u.

We prove the intermediate claim Lxv: SNo (x + v).

An exact proof term for the current goal is SNo_add_SNo x v Hx Hv1.

Apply SNoLtLe_or (x + v) u Lxv Hu1 to the current goal.

Assume H1: x + v < u.

An exact proof term for the current goal is H1.

Assume H1: u ≤ x + v.

We will prove False.

Apply HNC to the current goal.

Apply orIR to the current goal.

We use v to witness the existential quantifier.

Apply andI to the current goal.

We will prove v ∈ SNoL y.

An exact proof term for the current goal is Hv.

We will prove u ≤ x + v.

An exact proof term for the current goal is H1.

rewrite the current goal using add_SNo_eq x Hx y Hy (from right to left).

We will prove ∀z ∈ SNoR u, x + y < z.

Let z be given.

Assume Hz: z ∈ SNoR u.

Apply SNoR_E u Hu1 z Hz to the current goal.

Assume Hz1: SNo z.

Assume Hz2: SNoLev z ∈ SNoLev u.

Assume Hz3: u < z.

Apply SNoLt_trichotomy_or (x + y) z Lxy Hz1 to the current goal.

Assume H1.

Apply H1 to the current goal.

Assume H1: x + y < z.

An exact proof term for the current goal is H1.

Assume H1: x + y = z.

We will prove False.

Apply In_no2cycle (SNoLev z) (SNoLev u) Hz2 to the current goal.

We will prove SNoLev u ∈ SNoLev z.

rewrite the current goal using H1 (from right to left).

An exact proof term for the current goal is Hu2.

Assume H1: z < x + y.

We will prove False.

We prove the intermediate claim Lz1: z ∈ SNoS_ (SNoLev u).

An exact proof term for the current goal is SNoR_SNoS_ u z Hz.

We prove the intermediate claim Lz2: SNoLev z ∈ SNoLev (x + y).

Apply SNoLev_ordinal (x + y) Lxy to the current goal.

Assume Hxy1 _.

An exact proof term for the current goal is Hxy1 (SNoLev u) Hu2 (SNoLev z) Hz2.

Apply IH z Lz1 Lz2 H1 to the current goal.

Assume H2: ∃v ∈ SNoL x, z ≤ v + y.

Apply H2 to the current goal.

Let v be given.

Assume H3.

Apply H3 to the current goal.

Assume Hv: v ∈ SNoL x.

Assume H3: z ≤ v + y.

Apply SNoL_E x Hx v Hv to the current goal.

Assume Hv1: SNo v.

Assume Hv2: SNoLev v ∈ SNoLev x.

Assume Hv3: v < x.

Apply HNC to the current goal.

Apply orIL to the current goal.

We use v to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hv.

We will prove u ≤ v + y.

Apply SNoLe_tra u z (v + y) Hu1 Hz1 (SNo_add_SNo v y Hv1 Hy) to the current goal.

We will prove u ≤ z.

Apply SNoLtLe to the current goal.

An exact proof term for the current goal is Hz3.

We will prove z ≤ v + y.

An exact proof term for the current goal is H3.

Assume H2: ∃v ∈ SNoL y, z ≤ x + v.

Apply H2 to the current goal.

Let v be given.

Assume H3.

Apply H3 to the current goal.

Assume Hv: v ∈ SNoL y.

Assume H3: z ≤ x + v.

Apply SNoL_E y Hy v Hv to the current goal.

Assume Hv1: SNo v.

Assume Hv2: SNoLev v ∈ SNoLev y.

Assume Hv3: v < y.

Apply HNC to the current goal.

Apply orIR to the current goal.

We use v to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hv.

We will prove u ≤ x + v.

Apply SNoLe_tra u z (x + v) Hu1 Hz1 (SNo_add_SNo x v Hx Hv1) to the current goal.

We will prove u ≤ z.

Apply SNoLtLe to the current goal.

An exact proof term for the current goal is Hz3.

We will prove z ≤ x + v.

An exact proof term for the current goal is H3.