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) → x + y < z → (∃v ∈ SNoR x, v + y ≤ z) ∨ (∃v ∈ SNoR y, x + v ≤ z).

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

Assume Hu3: x + y < u.

Apply dneg to the current goal.

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

Apply SNoLt_irref u to the current goal.

We will prove u < u.

Apply (λH : u ≤ x + y ⇒ SNoLeLt_tra u (x + y) u Hu1 Lxy Hu1 H Hu3) to the current goal.

We will prove u ≤ x + y.

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 u ≤ SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2).

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

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

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

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

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

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

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

Let z be given.

Assume Hz: z ∈ SNoL u.

Apply SNoL_E u Hu1 z Hz to the current goal.

Assume Hz1: SNo z.

Assume Hz2: SNoLev z ∈ SNoLev u.

Assume Hz3: z < u.

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

Assume H1.

Apply H1 to the current goal.

Assume H1: z < x + y.

An exact proof term for the current goal is H1.

Assume H1: z = x + y.

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 left to right).

An exact proof term for the current goal is Hu2.

Assume H1: x + y < z.

We will prove False.

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

An exact proof term for the current goal is SNoL_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 ∈ SNoR x, v + y ≤ z.

Apply H2 to the current goal.

Let v be given.

Assume H3.

Apply H3 to the current goal.

Assume Hv: v ∈ SNoR x.

Assume H3: v + y ≤ z.

Apply SNoR_E x Hx v Hv to the current goal.

Assume Hv1: SNo v.

Assume Hv2: SNoLev v ∈ SNoLev x.

Assume Hv3: x < v.

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 v + y ≤ u.

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

We will prove v + y ≤ z.

An exact proof term for the current goal is H3.

We will prove z ≤ u.

Apply SNoLtLe to the current goal.

An exact proof term for the current goal is Hz3.

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

Apply H2 to the current goal.

Let v be given.

Assume H3.

Apply H3 to the current goal.

Assume Hv: v ∈ SNoR y.

Assume H3: x + v ≤ z.

Apply SNoR_E y Hy v Hv to the current goal.

Assume Hv1: SNo v.

Assume Hv2: SNoLev v ∈ SNoLev y.

Assume Hv3: y < v.

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 x + v ≤ u.

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

We will prove x + v ≤ z.

An exact proof term for the current goal is H3.

We will prove z ≤ u.

Apply SNoLtLe to the current goal.

An exact proof term for the current goal is Hz3.

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

We will prove ∀w ∈ Rxy1 ∪ Rxy2, u < w.

Let w be given.

Assume Hw: w ∈ Rxy1 ∪ Rxy2.

Apply binunionE Rxy1 Rxy2 w Hw to the current goal.

Assume Hw2: w ∈ Rxy1.

We will prove u < w.

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

Let v be given.

Assume Hv: v ∈ SNoR x.

Assume Hwv: w = v + y.

Apply SNoR_E x Hx v Hv to the current goal.

Assume Hv1: SNo v.

Assume Hv2: SNoLev v ∈ SNoLev x.

Assume Hv3: x < v.

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

We will prove u < v + y.

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 u (v + y) Hu1 Lvy to the current goal.

Assume H1: u < v + y.

An exact proof term for the current goal is H1.

Assume H1: v + y ≤ u.

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 ∈ SNoR x.

An exact proof term for the current goal is Hv.

We will prove v + y ≤ u.

An exact proof term for the current goal is H1.

Assume Hw2: w ∈ Rxy2.

We will prove u < w.

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

Let v be given.

Assume Hv: v ∈ SNoR y.

Assume Hwv: w = x + v.

Apply SNoR_E y Hy v Hv to the current goal.

Assume Hv1: SNo v.

Assume Hv2: SNoLev v ∈ SNoLev y.

Assume Hv3: y < v.

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

We will prove u < x + v.

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 u (x + v) Hu1 Lxv to the current goal.

Assume H1: u < x + v.

An exact proof term for the current goal is H1.

Assume H1: x + v ≤ u.

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 ∈ SNoR y.

An exact proof term for the current goal is Hv.

We will prove x + v ≤ u.

An exact proof term for the current goal is H1.