Let Lx, Rx, Ly, Ry, x and y be given.
Assume HLRx HLRy Hxe Hye.
Apply HLRx to the current goal.
Assume H.
Apply H to the current goal.
Assume HLRx1: ∀w ∈ Lx, SNo w.
Assume HLRx2: ∀z ∈ Rx, SNo z.
Assume HLRx3: ∀w ∈ Lx, ∀z ∈ Rx, w < z.
Apply HLRy to the current goal.
Assume H.
Apply H to the current goal.
Assume HLRy1: ∀w ∈ Ly, SNo w.
Assume HLRy2: ∀z ∈ Ry, SNo z.
Assume HLRy3: ∀w ∈ Ly, ∀z ∈ Ry, w < z.
Apply SNoCutP_SNoCut_impred Lx Rx HLRx to the current goal.
rewrite the current goal using Hxe (from right to left).
Assume Hx1: SNo x.
Assume Hx2: SNoLev x ∈ ordsucc ((⋃w ∈ Lxordsucc (SNoLev w)) ∪ (⋃z ∈ Rxordsucc (SNoLev z))).
Assume Hx3: ∀w ∈ Lx, w < x.
Assume Hx4: ∀z ∈ Rx, x < z.
Assume Hx5: (∀u, SNo u → (∀w ∈ Lx, w < u) → (∀z ∈ Rx, u < z) → SNoLev x ⊆ SNoLev u ∧ SNoEq_ (SNoLev x) x u).
Apply SNoCutP_SNoCut_impred Ly Ry HLRy to the current goal.
rewrite the current goal using Hye (from right to left).
Assume Hy1: SNo y.
Assume Hy2: SNoLev y ∈ ordsucc ((⋃w ∈ Lyordsucc (SNoLev w)) ∪ (⋃z ∈ Ryordsucc (SNoLev z))).
Assume Hy3: ∀w ∈ Ly, w < y.
Assume Hy4: ∀z ∈ Ry, y < z.
Assume Hy5: (∀u, SNo u → (∀w ∈ Ly, w < u) → (∀z ∈ Ry, u < z) → SNoLev y ⊆ SNoLev u ∧ SNoEq_ (SNoLev y) y u).
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx1 Hy1.
We prove the intermediate claim LI: ∀u, SNo u → SNoLev u ∈ SNoLev (x + y) → x + y < u → (∃v ∈ Rx, v + y ≤ u) ∨ (∃v ∈ Ry, x + v ≤ u).
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 ∈ Rx, v + y ≤ z) ∨ (∃v ∈ Ry, x + v ≤ z).
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: x + y < u.
Apply dneg to the current goal.
Assume HNC: ¬ ((∃v ∈ Rx, v + y ≤ u) ∨ (∃v ∈ Ry, 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 ∈ Lx}.
Set Lxy2 to be the term {x + w|w ∈ Ly}.
Set Rxy1 to be the term {z + y|z ∈ Rx}.
Set Rxy2 to be the term {x + z|z ∈ Ry}.
rewrite the current goal using add_SNoCut_eq Lx Rx Ly Ry x y HLRx HLRy Hxe Hye (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_SNoCutP_gen Lx Rx Ly Ry x y HLRx HLRy Hxe Hye.
rewrite the current goal using add_SNoCut_eq Lx Rx Ly Ry x y HLRx HLRy Hxe Hye (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 ∈ Rx, v + y ≤ z.
Apply H2 to the current goal.
Let v be given.
Assume H3.
Apply H3 to the current goal.
Assume Hv: v ∈ Rx.
Assume H3: v + y ≤ z.
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 (HLRx2 v Hv) Hy1) 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 ∈ Ry, x + v ≤ z.
Apply H2 to the current goal.
Let v be given.
Assume H3.
Apply H3 to the current goal.
Assume Hv: v ∈ Ry.
Assume H3: x + v ≤ z.
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 Hx1 (HLRy2 v Hv)) 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 Rx (λw ⇒ w + y) w Hw2 to the current goal.
Let v be given.
Assume Hv: v ∈ Rx.
Assume Hwv: w = v + y.
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 (HLRx2 v Hv) Hy1.
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 ∈ Rx.
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 Ry (λw ⇒ x + w) w Hw2 to the current goal.
Let v be given.
Assume Hv: v ∈ Ry.
Assume Hwv: w = x + 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 Hx1 (HLRy2 v Hv).
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 ∈ Ry.
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.
Let u be given.
Assume Hu: u ∈ SNoR (x + y).
Apply SNoR_E (x + y) Lxy u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: x + y < u.
An exact proof term for the current goal is LI u Hu1 Hu2 Hu3.
∎