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) → u < x + y → (∃v ∈ Lx, u ≤ v + y) ∨ (∃v ∈ Ly, u ≤ x + v).
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 ∈ Lx, z ≤ v + y) ∨ (∃v ∈ Ly, z ≤ x + v).
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: u < x + y.
Apply dneg to the current goal.
Assume HNC: ¬ ((∃v ∈ Lx, u ≤ v + y) ∨ (∃v ∈ Ly, 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 ∈ 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 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_SNoCutP_gen Lx Rx Ly Ry x y HLRx HLRy Hxe Hye.
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 Lx (λw ⇒ w + y) w Hw2 to the current goal.
Let v be given.
Assume Hv: v ∈ Lx.
Assume Hwv: w = v + y.
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 (HLRx1 v Hv) Hy1.
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 ∈ Lx.
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 Ly (λw ⇒ x + w) w Hw2 to the current goal.
Let v be given.
Assume Hv: v ∈ Ly.
Assume Hwv: w = x + v.
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 Hx1 (HLRy1 v Hv).
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 ∈ Ly.
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_SNoCut_eq Lx Rx Ly Ry x y HLRx HLRy Hxe Hye (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 ∈ Lx, z ≤ v + y.
Apply H2 to the current goal.
Let v be given.
Assume H3.
Apply H3 to the current goal.
Assume Hv: v ∈ Lx.
Assume H3: z ≤ v + y.
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 (HLRx1 v Hv) Hy1) 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 ∈ Ly, z ≤ x + v.
Apply H2 to the current goal.
Let v be given.
Assume H3.
Apply H3 to the current goal.
Assume Hv: v ∈ Ly.
Assume H3: z ≤ x + 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 u ≤ x + v.
Apply SNoLe_tra u z (x + v) Hu1 Hz1 (SNo_add_SNo x v Hx1 (HLRy1 v Hv)) 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.
Let u be given.
Assume Hu: u ∈ SNoL (x + y).
Apply SNoL_E (x + y) Lxy u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: u < x + y.
An exact proof term for the current goal is LI u Hu1 Hu2 Hu3.
∎