Let Lx, Rx, Ly and Ry be given.
Assume HLRx HLRy.
Let x and y be given.
Assume Hx Hy.
Set P1 to be the term λu ⇒ ∃v ∈ Lx, ∃w ∈ Ly, u + v * w ≤ v * y + x * w of type set → prop.
Set P2 to be the term λu ⇒ ∃v ∈ Rx, ∃w ∈ Ry, u + v * w ≤ v * y + x * w of type set → prop.
Set P to be the term λu ⇒ P1 u ∨ P2 u of type set → prop.
Apply HLRx to the current goal.
Assume H.
Apply H to the current goal.
Assume HLx HRx HLRx'.
Apply HLRy to the current goal.
Assume H.
Apply H to the current goal.
Assume HLy HRy HLRy'.
Apply SNoCutP_SNoCut_impred Lx Rx HLRx to the current goal.
rewrite the current goal using Hx (from right to left).
Assume Hx1: SNo x.
Assume Hx2: SNoLev x ∈ ordsucc ((⋃x ∈ Lxordsucc (SNoLev x)) ∪ (⋃y ∈ Rxordsucc (SNoLev y))).
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 Hy (from right to left).
Assume Hy1: SNo y.
Assume Hy2: SNoLev y ∈ ordsucc ((⋃y ∈ Lyordsucc (SNoLev y)) ∪ (⋃y ∈ Ryordsucc (SNoLev y))).
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_mul_SNo x y Hx1 Hy1.
We prove the intermediate claim LI: ∀u, SNo u → SNoLev u ∈ SNoLev (x * y) → u < x * y → P 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) → z < x * y → P z.
Assume Hu2: SNoLev u ∈ SNoLev (x * y).
Assume Hu3: u < x * y.
Apply dneg to the current goal.
Assume HNC: ¬ P u.
We prove the intermediate claim L1: ∀v ∈ Lx, ∀w ∈ Ly, v * y + x * w < u + v * w.
Let v be given.
Assume Hv.
Let w be given.
Assume Hw.
We prove the intermediate claim Lv1: SNo v.
An exact proof term for the current goal is HLx v Hv.
We prove the intermediate claim Lw1: SNo w.
An exact proof term for the current goal is HLy w Hw.
Apply SNoLtLe_or (v * y + x * w) (u + v * w) (SNo_add_SNo (v * y) (x * w) (SNo_mul_SNo v y Lv1 Hy1) (SNo_mul_SNo x w Hx1 Lw1)) (SNo_add_SNo u (v * w) Hu1 (SNo_mul_SNo v w Lv1 Lw1)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume H.
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 use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw.
An exact proof term for the current goal is H.
We prove the intermediate claim L2: ∀v ∈ Rx, ∀w ∈ Ry, v * y + x * w < u + v * w.
Let v be given.
Assume Hv.
Let w be given.
Assume Hw.
We prove the intermediate claim Lv1: SNo v.
An exact proof term for the current goal is HRx v Hv.
We prove the intermediate claim Lw1: SNo w.
An exact proof term for the current goal is HRy w Hw.
Apply SNoLtLe_or (v * y + x * w) (u + v * w) (SNo_add_SNo (v * y) (x * w) (SNo_mul_SNo v y Lv1 Hy1) (SNo_mul_SNo x w Hx1 Lw1)) (SNo_add_SNo u (v * w) Hu1 (SNo_mul_SNo v w Lv1 Lw1)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume H.
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 use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw.
An exact proof term for the current goal is H.
Apply SNoLt_irref u to the current goal.
Apply SNoLtLe_tra u (x * y) u Hu1 Lxy Hu1 Hu3 to the current goal.
We will prove x * y ≤ u.
Apply mul_SNoCut_abs Lx Rx Ly Ry x y HLRx HLRy Hx Hy to the current goal.
Let LxLy', RxRy', LxRy' and RxLy' be given.
Assume LxLy'E LxLy'I RxRy'E RxRy'I LxRy'E LxRy'I RxLy'E RxLy'I.
Assume HSC: SNoCutP (LxLy' ∪ RxRy') (LxRy' ∪ RxLy').
Assume HE: x * y = SNoCut (LxLy' ∪ RxRy') (LxRy' ∪ RxLy').
rewrite the current goal using HE (from left to right).
We will prove SNoCut (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') ≤ u.
rewrite the current goal using SNo_eta u Hu1 (from left to right).
We will prove SNoCut (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') ≤ SNoCut (SNoL u) (SNoR u).
Apply SNoCut_Le (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') (SNoL u) (SNoR u) HSC (SNoCutP_SNoL_SNoR u Hu1) to the current goal.
We will prove ∀z ∈ LxLy' ∪ RxRy', z < SNoCut (SNoL u) (SNoR u).
Let z be given.
rewrite the current goal using SNo_eta u Hu1 (from right to left).
Apply binunionE' to the current goal.
Assume Hz: z ∈ LxLy'.
Apply LxLy'E z Hz to the current goal.
Let w0 be given.
Assume Hw0.
Let w1 be given.
Assume Hw1.
Assume Hw0a Hw1a Hw0x Hw1y Hze.
rewrite the current goal using Hze (from left to right).
We will prove w0 * y + x * w1 + - w0 * w1 < u.
Apply add_SNo_minus_Lt1b3 (w0 * y) (x * w1) (w0 * w1) u (SNo_mul_SNo w0 y Hw0a Hy1) (SNo_mul_SNo x w1 Hx1 Hw1a) (SNo_mul_SNo w0 w1 Hw0a Hw1a) Hu1 to the current goal.
We will prove w0 * y + x * w1 < u + w0 * w1.
Apply SNoLtLe_or (w0 * y + x * w1) (u + w0 * w1) (SNo_add_SNo (w0 * y) (x * w1) (SNo_mul_SNo w0 y Hw0a Hy1) (SNo_mul_SNo x w1 Hx1 Hw1a)) (SNo_add_SNo u (w0 * w1) Hu1 (SNo_mul_SNo w0 w1 Hw0a Hw1a)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume H: u + w0 * w1 ≤ w0 * y + x * w1.
Apply HNC to the current goal.
We will prove P1 u ∨ P2 u.
Apply orIL to the current goal.
We will prove ∃v ∈ Lx, ∃w ∈ Ly, u + v * w ≤ v * y + x * w.
We use w0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw0.
We use w1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw1.
An exact proof term for the current goal is H.
Assume Hz: z ∈ RxRy'.
Apply RxRy'E z Hz to the current goal.
Let z0 be given.
Assume Hz0.
Let z1 be given.
Assume Hz1.
Assume Hz0a Hz1a Hz0x Hz1y Hze.
rewrite the current goal using Hze (from left to right).
We will prove z0 * y + x * z1 + - z0 * z1 < u.
Apply add_SNo_minus_Lt1b3 (z0 * y) (x * z1) (z0 * z1) u (SNo_mul_SNo z0 y Hz0a Hy1) (SNo_mul_SNo x z1 Hx1 Hz1a) (SNo_mul_SNo z0 z1 Hz0a Hz1a) Hu1 to the current goal.
We will prove z0 * y + x * z1 < u + z0 * z1.
Apply SNoLtLe_or (z0 * y + x * z1) (u + z0 * z1) (SNo_add_SNo (z0 * y) (x * z1) (SNo_mul_SNo z0 y Hz0a Hy1) (SNo_mul_SNo x z1 Hx1 Hz1a)) (SNo_add_SNo u (z0 * z1) Hu1 (SNo_mul_SNo z0 z1 Hz0a Hz1a)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume H: u + z0 * z1 ≤ z0 * y + x * z1.
Apply HNC to the current goal.
We will prove P1 u ∨ P2 u.
Apply orIR to the current goal.
We will prove ∃v ∈ Rx, ∃w ∈ Ry, u + v * w ≤ v * y + x * w.
We use z0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz0.
We use z1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz1.
An exact proof term for the current goal is H.
We will prove ∀z ∈ SNoR u, SNoCut (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') < z.
Let z be given.
Assume Hz: z ∈ SNoR u.
rewrite the current goal using HE (from right to left).
We will prove x * y < z.
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_impred z (x * y) Hz1 Lxy to the current goal.
Assume H1: z < x * y.
We prove the intermediate claim LPz: P z.
Apply IH z to the current goal.
We will prove z ∈ SNoS_ (SNoLev u).
Apply SNoS_I2 to the current goal.
An exact proof term for the current goal is Hz1.
An exact proof term for the current goal is Hu1.
An exact proof term for the current goal is Hz2.
We will prove SNoLev z ∈ SNoLev (x * y).
An exact proof term for the current goal is ordinal_TransSet (SNoLev (x * y)) (SNoLev_ordinal (x * y) Lxy) (SNoLev u) Hu2 (SNoLev z) Hz2.
We will prove z < x * y.
An exact proof term for the current goal is H1.
Apply LPz to the current goal.
Assume H2: P1 z.
Apply H2 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ Lx.
Assume H2.
Apply H2 to the current goal.
Let w be given.
Assume H2.
Apply H2 to the current goal.
Assume Hw: w ∈ Ly.
Assume Hvw: z + v * w ≤ v * y + x * w.
We prove the intermediate claim Lv1: SNo v.
An exact proof term for the current goal is HLx v Hv.
We prove the intermediate claim Lw1: SNo w.
An exact proof term for the current goal is HLy w Hw.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Lv1 Lw1.
We prove the intermediate claim L3: z + v * w < u + v * w.
Apply SNoLeLt_tra (z + v * w) (v * y + x * w) (u + v * w) (SNo_add_SNo z (v * w) Hz1 Lvw) (SNo_add_SNo (v * y) (x * w) (SNo_mul_SNo v y Lv1 Hy1) (SNo_mul_SNo x w Hx1 Lw1)) (SNo_add_SNo u (v * w) Hu1 Lvw) Hvw to the current goal.
We will prove v * y + x * w < u + v * w.
An exact proof term for the current goal is L1 v Hv w Hw.
We prove the intermediate claim L4: z < u.
An exact proof term for the current goal is add_SNo_Lt1_cancel z (v * w) u Hz1 Lvw Hu1 L3.
We will prove False.
Apply SNoLt_irref u to the current goal.
An exact proof term for the current goal is SNoLt_tra u z u Hu1 Hz1 Hu1 Hz3 L4.
Assume H2: P2 z.
Apply H2 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ Rx.
Assume H2.
Apply H2 to the current goal.
Let w be given.
Assume H2.
Apply H2 to the current goal.
Assume Hw: w ∈ Ry.
Assume Hvw: z + v * w ≤ v * y + x * w.
We prove the intermediate claim Lv1: SNo v.
An exact proof term for the current goal is HRx v Hv.
We prove the intermediate claim Lw1: SNo w.
An exact proof term for the current goal is HRy w Hw.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Lv1 Lw1.
We prove the intermediate claim L5: z + v * w < u + v * w.
Apply SNoLeLt_tra (z + v * w) (v * y + x * w) (u + v * w) (SNo_add_SNo z (v * w) Hz1 Lvw) (SNo_add_SNo (v * y) (x * w) (SNo_mul_SNo v y Lv1 Hy1) (SNo_mul_SNo x w Hx1 Lw1)) (SNo_add_SNo u (v * w) Hu1 Lvw) Hvw to the current goal.
We will prove v * y + x * w < u + v * w.
An exact proof term for the current goal is L2 v Hv w Hw.
We prove the intermediate claim L6: z < u.
An exact proof term for the current goal is add_SNo_Lt1_cancel z (v * w) u Hz1 Lvw Hu1 L5.
We will prove False.
Apply SNoLt_irref u to the current goal.
An exact proof term for the current goal is SNoLt_tra u z u Hu1 Hz1 Hu1 Hz3 L6.
Assume H1: z = x * y.
Apply In_no2cycle (SNoLev u) (SNoLev (x * y)) Hu2 to the current goal.
We will prove SNoLev (x * y) ∈ SNoLev u.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hz2.
Assume H1: x * y < z.
An exact proof term for the current goal is H1.
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.
∎