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).
Set LxLy' to be the term {w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ly}.
Set RxRy' to be the term {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ry}.
Set LxRy' to be the term {w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ry}.
Set RxLy' to be the term {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ly}.
We prove the intermediate claim LxLy'E: ∀u ∈ LxLy', ∀p : prop, (∀w ∈ Lx, ∀w' ∈ Ly, SNo w → SNo w' → w < x → w' < y → u = w * y + x * w' + - w * w' → p) → p.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Apply ReplE_impred (Lx ⨯ Ly) (λw ⇒ (w 0) * y + x * (w 1) + - (w 0) * (w 1)) u Hu to the current goal.
Let ww' be given.
Assume Hww': ww' ∈ Lx ⨯ Ly.
Assume Hue: u = (ww' 0) * y + x * (ww' 1) + - (ww' 0) * (ww' 1).
We prove the intermediate claim Lww'0: ww' 0 ∈ Lx.
An exact proof term for the current goal is ap0_Sigma Lx (λ_ ⇒ Ly) ww' Hww'.
We prove the intermediate claim Lww'1: ww' 1 ∈ Ly.
An exact proof term for the current goal is ap1_Sigma Lx (λ_ ⇒ Ly) ww' Hww'.
Apply Hp (ww' 0) Lww'0 (ww' 1) Lww'1 to the current goal.
We will prove SNo (ww' 0).
An exact proof term for the current goal is HLRx1 (ww' 0) Lww'0.
We will prove SNo (ww' 1).
An exact proof term for the current goal is HLRy1 (ww' 1) Lww'1.
We will prove ww' 0 < x.
An exact proof term for the current goal is Hx3 (ww' 0) Lww'0.
We will prove ww' 1 < y.
An exact proof term for the current goal is Hy3 (ww' 1) Lww'1.
An exact proof term for the current goal is Hue.
We prove the intermediate claim LxLy'I: ∀w ∈ Lx, ∀w' ∈ Ly, w * y + x * w' + - w * w' ∈ LxLy'.
Let w be given.
Assume Hw.
Let w' be given.
Assume Hw'.
rewrite the current goal using tuple_2_0_eq w w' (from right to left).
rewrite the current goal using tuple_2_1_eq w w' (from right to left) at positions 2 and 4.
Apply ReplI (Lx ⨯ Ly) (λw ⇒ w 0 * y + x * w 1 + - w 0 * w 1) (w,w') to the current goal.
We will prove (w,w') ∈ Lx ⨯ Ly.
An exact proof term for the current goal is tuple_2_setprod Lx Ly w Hw w' Hw'.
We prove the intermediate claim RxRy'E: ∀u ∈ RxRy', ∀p : prop, (∀z ∈ Rx, ∀z' ∈ Ry, SNo z → SNo z' → x < z → y < z' → u = z * y + x * z' + - z * z' → p) → p.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Apply ReplE_impred (Rx ⨯ Ry) (λz ⇒ (z 0) * y + x * (z 1) + - (z 0) * (z 1)) u Hu to the current goal.
Let zz' be given.
Assume Hzz': zz' ∈ Rx ⨯ Ry.
Assume Hue: u = (zz' 0) * y + x * (zz' 1) + - (zz' 0) * (zz' 1).
We prove the intermediate claim Lzz'0: zz' 0 ∈ Rx.
An exact proof term for the current goal is ap0_Sigma Rx (λ_ ⇒ Ry) zz' Hzz'.
We prove the intermediate claim Lzz'1: zz' 1 ∈ Ry.
An exact proof term for the current goal is ap1_Sigma Rx (λ_ ⇒ Ry) zz' Hzz'.
Apply Hp (zz' 0) Lzz'0 (zz' 1) Lzz'1 to the current goal.
We will prove SNo (zz' 0).
An exact proof term for the current goal is HLRx2 (zz' 0) Lzz'0.
We will prove SNo (zz' 1).
An exact proof term for the current goal is HLRy2 (zz' 1) Lzz'1.
We will prove x < zz' 0.
An exact proof term for the current goal is Hx4 (zz' 0) Lzz'0.
We will prove y < zz' 1.
An exact proof term for the current goal is Hy4 (zz' 1) Lzz'1.
An exact proof term for the current goal is Hue.
We prove the intermediate claim RxRy'I: ∀z ∈ Rx, ∀z' ∈ Ry, z * y + x * z' + - z * z' ∈ RxRy'.
Let z be given.
Assume Hz.
Let z' be given.
Assume Hz'.
rewrite the current goal using tuple_2_0_eq z z' (from right to left).
rewrite the current goal using tuple_2_1_eq z z' (from right to left) at positions 2 and 4.
Apply ReplI (Rx ⨯ Ry) (λz ⇒ z 0 * y + x * z 1 + - z 0 * z 1) (z,z') to the current goal.
We will prove (z,z') ∈ Rx ⨯ Ry.
An exact proof term for the current goal is tuple_2_setprod Rx Ry z Hz z' Hz'.
We prove the intermediate claim LxRy'E: ∀u ∈ LxRy', ∀p : prop, (∀w ∈ Lx, ∀z ∈ Ry, SNo w → SNo z → w < x → y < z → u = w * y + x * z + - w * z → p) → p.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Apply ReplE_impred (Lx ⨯ Ry) (λw ⇒ (w 0) * y + x * (w 1) + - (w 0) * (w 1)) u Hu to the current goal.
Let wz be given.
Assume Hwz: wz ∈ Lx ⨯ Ry.
Assume Hue: u = (wz 0) * y + x * (wz 1) + - (wz 0) * (wz 1).
We prove the intermediate claim Lwz0: wz 0 ∈ Lx.
An exact proof term for the current goal is ap0_Sigma Lx (λ_ ⇒ Ry) wz Hwz.
We prove the intermediate claim Lwz1: wz 1 ∈ Ry.
An exact proof term for the current goal is ap1_Sigma Lx (λ_ ⇒ Ry) wz Hwz.
Apply Hp (wz 0) Lwz0 (wz 1) Lwz1 to the current goal.
We will prove SNo (wz 0).
An exact proof term for the current goal is HLRx1 (wz 0) Lwz0.
We will prove SNo (wz 1).
An exact proof term for the current goal is HLRy2 (wz 1) Lwz1.
We will prove wz 0 < x.
An exact proof term for the current goal is Hx3 (wz 0) Lwz0.
We will prove y < wz 1.
An exact proof term for the current goal is Hy4 (wz 1) Lwz1.
An exact proof term for the current goal is Hue.
We prove the intermediate claim LxRy'I: ∀w ∈ Lx, ∀z ∈ Ry, w * y + x * z + - w * z ∈ LxRy'.
Let w be given.
Assume Hw.
Let z be given.
Assume Hz.
rewrite the current goal using tuple_2_0_eq w z (from right to left).
rewrite the current goal using tuple_2_1_eq w z (from right to left) at positions 2 and 4.
Apply ReplI (Lx ⨯ Ry) (λw ⇒ w 0 * y + x * w 1 + - w 0 * w 1) (w,z) to the current goal.
We will prove (w,z) ∈ Lx ⨯ Ry.
An exact proof term for the current goal is tuple_2_setprod Lx Ry w Hw z Hz.
We prove the intermediate claim RxLy'E: ∀u ∈ RxLy', ∀p : prop, (∀z ∈ Rx, ∀w ∈ Ly, SNo z → SNo w → x < z → w < y → u = z * y + x * w + - z * w → p) → p.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Apply ReplE_impred (Rx ⨯ Ly) (λz ⇒ (z 0) * y + x * (z 1) + - (z 0) * (z 1)) u Hu to the current goal.
Let zw be given.
Assume Hzw: zw ∈ Rx ⨯ Ly.
Assume Hue: u = (zw 0) * y + x * (zw 1) + - (zw 0) * (zw 1).
We prove the intermediate claim Lzw0: zw 0 ∈ Rx.
An exact proof term for the current goal is ap0_Sigma Rx (λ_ ⇒ Ly) zw Hzw.
We prove the intermediate claim Lzw1: zw 1 ∈ Ly.
An exact proof term for the current goal is ap1_Sigma Rx (λ_ ⇒ Ly) zw Hzw.
Apply Hp (zw 0) Lzw0 (zw 1) Lzw1 to the current goal.
We will prove SNo (zw 0).
An exact proof term for the current goal is HLRx2 (zw 0) Lzw0.
We will prove SNo (zw 1).
An exact proof term for the current goal is HLRy1 (zw 1) Lzw1.
We will prove x < zw 0.
An exact proof term for the current goal is Hx4 (zw 0) Lzw0.
We will prove zw 1 < y.
An exact proof term for the current goal is Hy3 (zw 1) Lzw1.
An exact proof term for the current goal is Hue.
We prove the intermediate claim RxLy'I: ∀z ∈ Rx, ∀w ∈ Ly, z * y + x * w + - z * w ∈ RxLy'.
Let z be given.
Assume Hz.
Let w be given.
Assume Hw.
rewrite the current goal using tuple_2_0_eq z w (from right to left).
rewrite the current goal using tuple_2_1_eq z w (from right to left) at positions 2 and 4.
Apply ReplI (Rx ⨯ Ly) (λw ⇒ w 0 * y + x * w 1 + - w 0 * w 1) (z,w) to the current goal.
We will prove (z,w) ∈ Rx ⨯ Ly.
An exact proof term for the current goal is tuple_2_setprod Rx Ly z Hz w Hw.
We prove the intermediate claim L1: SNoCutP (LxLy' ∪ RxRy') (LxRy' ∪ RxLy').
We will prove (∀w ∈ LxLy' ∪ RxRy', SNo w) ∧ (∀z ∈ LxRy' ∪ RxLy', SNo z) ∧ (∀w ∈ LxLy' ∪ RxRy', ∀z ∈ LxRy' ∪ RxLy', w < z).
Apply and3I to the current goal.
Let w be given.
Apply binunionE' to the current goal.
Assume Hw: w ∈ LxLy'.
Apply LxLy'E w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ Lx.
Let w'' be given.
Assume Hw'': w'' ∈ Ly.
Assume Hw'1: SNo w'.
Assume Hw''1: SNo w''.
Assume Hw'2: w' < x.
Assume Hw''2: w'' < y.
Assume Hwe.
rewrite the current goal using Hwe (from left to right).
We will prove SNo (w' * y + x * w'' + - w' * w'').
Apply SNo_add_SNo_3 to the current goal.
An exact proof term for the current goal is SNo_mul_SNo w' y Hw'1 Hy1.
An exact proof term for the current goal is SNo_mul_SNo x w'' Hx1 Hw''1.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is SNo_mul_SNo w' w'' Hw'1 Hw''1.
Assume Hw: w ∈ RxRy'.
Apply RxRy'E w Hw to the current goal.
Let z' be given.
Assume Hz': z' ∈ Rx.
Let z'' be given.
Assume Hz'': z'' ∈ Ry.
Assume Hz'1: SNo z'.
Assume Hz''1: SNo z''.
Assume Hz'2: x < z'.
Assume Hz''2: y < z''.
Assume Hwe.
rewrite the current goal using Hwe (from left to right).
We will prove SNo (z' * y + x * z'' + - z' * z'').
Apply SNo_add_SNo_3 to the current goal.
An exact proof term for the current goal is SNo_mul_SNo z' y Hz'1 Hy1.
An exact proof term for the current goal is SNo_mul_SNo x z'' Hx1 Hz''1.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is SNo_mul_SNo z' z'' Hz'1 Hz''1.
Let z be given.
Apply binunionE' to the current goal.
Assume Hz: z ∈ LxRy'.
Apply LxRy'E z Hz to the current goal.
Let w' be given.
Assume Hw': w' ∈ Lx.
Let z' be given.
Assume Hz': z' ∈ Ry.
Assume Hw'1: SNo w'.
Assume Hz'1: SNo z'.
Assume Hw'2: w' < x.
Assume Hz'2: y < z'.
Assume Hze.
rewrite the current goal using Hze (from left to right).
We will prove SNo (w' * y + x * z' + - w' * z').
Apply SNo_add_SNo_3 to the current goal.
An exact proof term for the current goal is SNo_mul_SNo w' y Hw'1 Hy1.
An exact proof term for the current goal is SNo_mul_SNo x z' Hx1 Hz'1.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is SNo_mul_SNo w' z' Hw'1 Hz'1.
Assume Hz: z ∈ RxLy'.
Apply RxLy'E z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Rx.
Let w' be given.
Assume Hw': w' ∈ Ly.
Assume Hz'1: SNo z'.
Assume Hw'1: SNo w'.
Assume Hz'2: x < z'.
Assume Hw'2: w' < y.
Assume Hze.
rewrite the current goal using Hze (from left to right).
We will prove SNo (z' * y + x * w' + - z' * w').
Apply SNo_add_SNo_3 to the current goal.
An exact proof term for the current goal is SNo_mul_SNo z' y Hz'1 Hy1.
An exact proof term for the current goal is SNo_mul_SNo x w' Hx1 Hw'1.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is SNo_mul_SNo z' w' Hz'1 Hw'1.
Let w be given.
Apply binunionE' to the current goal.
Assume Hw: w ∈ LxLy'.
Apply LxLy'E w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ Lx.
Let w'' be given.
Assume Hw'': w'' ∈ Ly.
Assume Hw'1: SNo w'.
Assume Hw''1: SNo w''.
Assume Hw'2: w' < x.
Assume Hw''2: w'' < y.
Assume Hwe.
rewrite the current goal using Hwe (from left to right).
Let z be given.
Apply binunionE' to the current goal.
Assume Hz: z ∈ LxRy'.
Apply LxRy'E z Hz to the current goal.
Let w''' be given.
Assume Hw''': w''' ∈ Lx.
Let z' be given.
Assume Hz': z' ∈ Ry.
Assume Hw'''1: SNo w'''.
Assume Hz'1: SNo z'.
Assume Hw'''2: w''' < x.
Assume Hz'2: y < z'.
Assume Hze.
rewrite the current goal using Hze (from left to right).
We will prove w' * y + x * w'' + - w' * w'' < w''' * y + x * z' + - w''' * z'.
Apply add_SNo_minus_Lt12b3 (w' * y) (x * w'') (w' * w'') (w''' * y) (x * z') (w''' * z') (SNo_mul_SNo w' y Hw'1 Hy1) (SNo_mul_SNo x w'' Hx1 Hw''1) (SNo_mul_SNo w' w'' Hw'1 Hw''1) (SNo_mul_SNo w''' y Hw'''1 Hy1) (SNo_mul_SNo x z' Hx1 Hz'1) (SNo_mul_SNo w''' z' Hw'''1 Hz'1) to the current goal.
We will prove w' * y + x * w'' + w''' * z' < w''' * y + x * z' + w' * w''.
Apply SNoLt_tra (w' * y + x * w'' + w''' * z') (x * y + w' * w'' + w''' * z') (w''' * y + x * z' + w' * w'') (SNo_add_SNo_3 (w' * y) (x * w'') (w''' * z') (SNo_mul_SNo w' y Hw'1 Hy1) (SNo_mul_SNo x w'' Hx1 Hw''1) (SNo_mul_SNo w''' z' Hw'''1 Hz'1)) (SNo_add_SNo_3 (x * y) (w' * w'') (w''' * z') (SNo_mul_SNo x y Hx1 Hy1) (SNo_mul_SNo w' w'' Hw'1 Hw''1) (SNo_mul_SNo w''' z' Hw'''1 Hz'1)) (SNo_add_SNo_3 (w''' * y) (x * z') (w' * w'') (SNo_mul_SNo w''' y Hw'''1 Hy1) (SNo_mul_SNo x z' Hx1 Hz'1) (SNo_mul_SNo w' w'' Hw'1 Hw''1)) to the current goal.
We will prove w' * y + x * w'' + w''' * z' < x * y + w' * w'' + w''' * z'.
rewrite the current goal using add_SNo_rotate_3_1 (w' * y) (x * w'') (w''' * z') (SNo_mul_SNo w' y Hw'1 Hy1) (SNo_mul_SNo x w'' Hx1 Hw''1) (SNo_mul_SNo w''' z' Hw'''1 Hz'1) (from left to right).
rewrite the current goal using add_SNo_rotate_3_1 (x * y) (w' * w'') (w''' * z') (SNo_mul_SNo x y Hx1 Hy1) (SNo_mul_SNo w' w'' Hw'1 Hw''1) (SNo_mul_SNo w''' z' Hw'''1 Hz'1) (from left to right).
We will prove w''' * z' + w' * y + x * w'' < w''' * z' + x * y + w' * w''.
Apply add_SNo_Lt2 (w''' * z') (w' * y + x * w'') (x * y + w' * w'') (SNo_mul_SNo w''' z' Hw'''1 Hz'1) (SNo_add_SNo (w' * y) (x * w'') (SNo_mul_SNo w' y Hw'1 Hy1) (SNo_mul_SNo x w'' Hx1 Hw''1)) (SNo_add_SNo (x * y) (w' * w'') (SNo_mul_SNo x y Hx1 Hy1) (SNo_mul_SNo w' w'' Hw'1 Hw''1)) to the current goal.
We will prove w' * y + x * w'' < x * y + w' * w''.
An exact proof term for the current goal is mul_SNo_Lt x y w' w'' Hx1 Hy1 Hw'1 Hw''1 Hw'2 Hw''2.
We will prove x * y + w' * w'' + w''' * z' < w''' * y + x * z' + w' * w''.
rewrite the current goal using add_SNo_com_3_0_1 (x * y) (w' * w'') (w''' * z') (SNo_mul_SNo x y Hx1 Hy1) (SNo_mul_SNo w' w'' Hw'1 Hw''1) (SNo_mul_SNo w''' z' Hw'''1 Hz'1) (from left to right).
rewrite the current goal using add_SNo_rotate_3_1 (w''' * y) (x * z') (w' * w'') (SNo_mul_SNo w''' y Hw'''1 Hy1) (SNo_mul_SNo x z' Hx1 Hz'1) (SNo_mul_SNo w' w'' Hw'1 Hw''1) (from left to right).
We will prove w' * w'' + x * y + w''' * z' < w' * w'' + w''' * y + x * z'.
Apply add_SNo_Lt2 (w' * w'') (x * y + w''' * z') (w''' * y + x * z') (SNo_mul_SNo w' w'' Hw'1 Hw''1) (SNo_add_SNo (x * y) (w''' * z') (SNo_mul_SNo x y Hx1 Hy1) (SNo_mul_SNo w''' z' Hw'''1 Hz'1)) (SNo_add_SNo (w''' * y) (x * z') (SNo_mul_SNo w''' y Hw'''1 Hy1) (SNo_mul_SNo x z' Hx1 Hz'1)) to the current goal.
We will prove x * y + w''' * z' < w''' * y + x * z'.
rewrite the current goal using add_SNo_com (x * y) (w''' * z') (SNo_mul_SNo x y Hx1 Hy1) (SNo_mul_SNo w''' z' Hw'''1 Hz'1) (from left to right).
rewrite the current goal using add_SNo_com (w''' * y) (x * z') (SNo_mul_SNo w''' y Hw'''1 Hy1) (SNo_mul_SNo x z' Hx1 Hz'1) (from left to right).
We will prove w''' * z' + x * y < x * z' + w''' * y.
An exact proof term for the current goal is mul_SNo_Lt x z' w''' y Hx1 Hz'1 Hw'''1 Hy1 Hw'''2 Hz'2.
Assume Hz: z ∈ RxLy'.
Apply RxLy'E z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Rx.
Let w''' be given.
Assume Hw''': w''' ∈ Ly.
Assume Hz'1: SNo z'.
Assume Hw'''1: SNo w'''.
Assume Hz'2: x < z'.
Assume Hw'''2: w''' < y.
Assume Hze.
rewrite the current goal using Hze (from left to right).
We will prove w' * y + x * w'' + - w' * w'' < z' * y + x * w''' + - z' * w'''.
Apply add_SNo_minus_Lt12b3 (w' * y) (x * w'') (w' * w'') (z' * y) (x * w''') (z' * w''') (SNo_mul_SNo w' y Hw'1 Hy1) (SNo_mul_SNo x w'' Hx1 Hw''1) (SNo_mul_SNo w' w'' Hw'1 Hw''1) (SNo_mul_SNo z' y Hz'1 Hy1) (SNo_mul_SNo x w''' Hx1 Hw'''1) (SNo_mul_SNo z' w''' Hz'1 Hw'''1) to the current goal.
We will prove w' * y + x * w'' + z' * w''' < z' * y + x * w''' + w' * w''.
Apply SNoLt_tra (w' * y + x * w'' + z' * w''') (z' * w''' + x * y + w' * w'') (z' * y + x * w''' + w' * w'') (SNo_add_SNo_3 (w' * y) (x * w'') (z' * w''') (SNo_mul_SNo w' y Hw'1 Hy1) (SNo_mul_SNo x w'' Hx1 Hw''1) (SNo_mul_SNo z' w''' Hz'1 Hw'''1)) (SNo_add_SNo_3 (z' * w''') (x * y) (w' * w'') (SNo_mul_SNo z' w''' Hz'1 Hw'''1) (SNo_mul_SNo x y Hx1 Hy1) (SNo_mul_SNo w' w'' Hw'1 Hw''1)) (SNo_add_SNo_3 (z' * y) (x * w''') (w' * w'') (SNo_mul_SNo z' y Hz'1 Hy1) (SNo_mul_SNo x w''' Hx1 Hw'''1) (SNo_mul_SNo w' w'' Hw'1 Hw''1)) to the current goal.
We will prove w' * y + x * w'' + z' * w''' < z' * w''' + x * y + w' * w''.
rewrite the current goal using add_SNo_rotate_3_1 (w' * y) (x * w'') (z' * w''') (SNo_mul_SNo w' y Hw'1 Hy1) (SNo_mul_SNo x w'' Hx1 Hw''1) (SNo_mul_SNo z' w''' Hz'1 Hw'''1) (from left to right).
We will prove z' * w''' + w' * y + x * w'' < z' * w''' + x * y + w' * w''.
Apply add_SNo_Lt2 (z' * w''') (w' * y + x * w'') (x * y + w' * w'') (SNo_mul_SNo z' w''' Hz'1 Hw'''1) (SNo_add_SNo (w' * y) (x * w'') (SNo_mul_SNo w' y Hw'1 Hy1) (SNo_mul_SNo x w'' Hx1 Hw''1)) (SNo_add_SNo (x * y) (w' * w'') (SNo_mul_SNo x y Hx1 Hy1) (SNo_mul_SNo w' w'' Hw'1 Hw''1)) to the current goal.
We will prove w' * y + x * w'' < x * y + w' * w''.
An exact proof term for the current goal is mul_SNo_Lt x y w' w'' Hx1 Hy1 Hw'1 Hw''1 Hw'2 Hw''2.
We will prove z' * w''' + x * y + w' * w'' < z' * y + x * w''' + w' * w''.
rewrite the current goal using add_SNo_rotate_3_1 (z' * w''') (x * y) (w' * w'') (SNo_mul_SNo z' w''' Hz'1 Hw'''1) (SNo_mul_SNo x y Hx1 Hy1) (SNo_mul_SNo w' w'' Hw'1 Hw''1) (from left to right).
rewrite the current goal using add_SNo_rotate_3_1 (z' * y) (x * w''') (w' * w'') (SNo_mul_SNo z' y Hz'1 Hy1) (SNo_mul_SNo x w''' Hx1 Hw'''1) (SNo_mul_SNo w' w'' Hw'1 Hw''1) (from left to right).
We will prove w' * w'' + z' * w''' + x * y < w' * w'' + z' * y + x * w'''.
Apply add_SNo_Lt2 (w' * w'') (z' * w''' + x * y) (z' * y + x * w''') (SNo_mul_SNo w' w'' Hw'1 Hw''1) (SNo_add_SNo (z' * w''') (x * y) (SNo_mul_SNo z' w''' Hz'1 Hw'''1) (SNo_mul_SNo x y Hx1 Hy1)) (SNo_add_SNo (z' * y) (x * w''') (SNo_mul_SNo z' y Hz'1 Hy1) (SNo_mul_SNo x w''' Hx1 Hw'''1)) to the current goal.
We will prove z' * w''' + x * y < z' * y + x * w'''.
rewrite the current goal using add_SNo_com (z' * w''') (x * y) (SNo_mul_SNo z' w''' Hz'1 Hw'''1) (SNo_mul_SNo x y Hx1 Hy1) (from left to right).
We will prove x * y + z' * w''' < z' * y + x * w'''.
An exact proof term for the current goal is mul_SNo_Lt z' y x w''' Hz'1 Hy1 Hx1 Hw'''1 Hz'2 Hw'''2.
Assume Hw: w ∈ RxRy'.
Apply RxRy'E w Hw to the current goal.
Let z' be given.
Assume Hz': z' ∈ Rx.
Let z'' be given.
Assume Hz'': z'' ∈ Ry.
Assume Hz'1: SNo z'.
Assume Hz''1: SNo z''.
Assume Hz'2: x < z'.
Assume Hz''2: y < z''.
Assume Hwe.
rewrite the current goal using Hwe (from left to right).
Let z be given.
Apply binunionE' to the current goal.
Assume Hz: z ∈ LxRy'.
Apply LxRy'E z Hz to the current goal.
Let w' be given.
Assume Hw': w' ∈ Lx.
Let z''' be given.
Assume Hz''': z''' ∈ Ry.
Assume Hw'1: SNo w'.
Assume Hz'''1: SNo z'''.
Assume Hw'2: w' < x.
Assume Hz'''2: y < z'''.
Assume Hze.
rewrite the current goal using Hze (from left to right).
We will prove z' * y + x * z'' + - z' * z'' < w' * y + x * z''' + - w' * z'''.
Apply add_SNo_minus_Lt12b3 (z' * y) (x * z'') (z' * z'') (w' * y) (x * z''') (w' * z''') (SNo_mul_SNo z' y Hz'1 Hy1) (SNo_mul_SNo x z'' Hx1 Hz''1) (SNo_mul_SNo z' z'' Hz'1 Hz''1) (SNo_mul_SNo w' y Hw'1 Hy1) (SNo_mul_SNo x z''' Hx1 Hz'''1) (SNo_mul_SNo w' z''' Hw'1 Hz'''1) to the current goal.
We will prove z' * y + x * z'' + w' * z''' < w' * y + x * z''' + z' * z''.
Apply SNoLt_tra (z' * y + x * z'' + w' * z''') (w' * z''' + z' * z'' + x * y) (w' * y + x * z''' + z' * z'') (SNo_add_SNo_3 (z' * y) (x * z'') (w' * z''') (SNo_mul_SNo z' y Hz'1 Hy1) (SNo_mul_SNo x z'' Hx1 Hz''1) (SNo_mul_SNo w' z''' Hw'1 Hz'''1)) (SNo_add_SNo_3 (w' * z''') (z' * z'') (x * y) (SNo_mul_SNo w' z''' Hw'1 Hz'''1) (SNo_mul_SNo z' z'' Hz'1 Hz''1) (SNo_mul_SNo x y Hx1 Hy1)) (SNo_add_SNo_3 (w' * y) (x * z''') (z' * z'') (SNo_mul_SNo w' y Hw'1 Hy1) (SNo_mul_SNo x z''' Hx1 Hz'''1) (SNo_mul_SNo z' z'' Hz'1 Hz''1)) to the current goal.
We will prove z' * y + x * z'' + w' * z''' < w' * z''' + z' * z'' + x * y.
rewrite the current goal using add_SNo_rotate_3_1 (z' * y) (x * z'') (w' * z''') (SNo_mul_SNo z' y Hz'1 Hy1) (SNo_mul_SNo x z'' Hx1 Hz''1) (SNo_mul_SNo w' z''' Hw'1 Hz'''1) (from left to right).
We will prove w' * z''' + z' * y + x * z'' < w' * z''' + z' * z'' + x * y.
Apply add_SNo_Lt2 (w' * z''') (z' * y + x * z'') (z' * z'' + x * y) (SNo_mul_SNo w' z''' Hw'1 Hz'''1) (SNo_add_SNo (z' * y) (x * z'') (SNo_mul_SNo z' y Hz'1 Hy1) (SNo_mul_SNo x z'' Hx1 Hz''1)) (SNo_add_SNo (z' * z'') (x * y) (SNo_mul_SNo z' z'' Hz'1 Hz''1) (SNo_mul_SNo x y Hx1 Hy1)) to the current goal.
We will prove z' * y + x * z'' < z' * z'' + x * y.
rewrite the current goal using add_SNo_com (z' * y) (x * z'') (SNo_mul_SNo z' y Hz'1 Hy1) (SNo_mul_SNo x z'' Hx1 Hz''1) (from left to right).
An exact proof term for the current goal is mul_SNo_Lt z' z'' x y Hz'1 Hz''1 Hx1 Hy1 Hz'2 Hz''2.
We will prove w' * z''' + z' * z'' + x * y < w' * y + x * z''' + z' * z''.
rewrite the current goal using add_SNo_com_3_0_1 (w' * z''') (z' * z'') (x * y) (SNo_mul_SNo w' z''' Hw'1 Hz'''1) (SNo_mul_SNo z' z'' Hz'1 Hz''1) (SNo_mul_SNo x y Hx1 Hy1) (from left to right).
rewrite the current goal using add_SNo_rotate_3_1 (w' * y) (x * z''') (z' * z'') (SNo_mul_SNo w' y Hw'1 Hy1) (SNo_mul_SNo x z''' Hx1 Hz'''1) (SNo_mul_SNo z' z'' Hz'1 Hz''1) (from left to right).
We will prove z' * z'' + w' * z''' + x * y < z' * z'' + w' * y + x * z'''.
Apply add_SNo_Lt2 (z' * z'') (w' * z''' + x * y) (w' * y + x * z''') (SNo_mul_SNo z' z'' Hz'1 Hz''1) (SNo_add_SNo (w' * z''') (x * y) (SNo_mul_SNo w' z''' Hw'1 Hz'''1) (SNo_mul_SNo x y Hx1 Hy1)) (SNo_add_SNo (w' * y) (x * z''') (SNo_mul_SNo w' y Hw'1 Hy1) (SNo_mul_SNo x z''' Hx1 Hz'''1)) to the current goal.
We will prove w' * z''' + x * y < w' * y + x * z'''.
rewrite the current goal using add_SNo_com (w' * y) (x * z''') (SNo_mul_SNo w' y Hw'1 Hy1) (SNo_mul_SNo x z''' Hx1 Hz'''1) (from left to right).
An exact proof term for the current goal is mul_SNo_Lt x z''' w' y Hx1 Hz'''1 Hw'1 Hy1 Hw'2 Hz'''2.
Assume Hz: z ∈ RxLy'.
Apply RxLy'E z Hz to the current goal.
Let z''' be given.
Assume Hz''': z''' ∈ Rx.
Let w' be given.
Assume Hw': w' ∈ Ly.
Assume Hz'''1: SNo z'''.
Assume Hw'1: SNo w'.
Assume Hz'''2: x < z'''.
Assume Hw'2: w' < y.
Assume Hze.
rewrite the current goal using Hze (from left to right).
We will prove z' * y + x * z'' + - z' * z'' < z''' * y + x * w' + - z''' * w'.
Apply add_SNo_minus_Lt12b3 (z' * y) (x * z'') (z' * z'') (z''' * y) (x * w') (z''' * w') (SNo_mul_SNo z' y Hz'1 Hy1) (SNo_mul_SNo x z'' Hx1 Hz''1) (SNo_mul_SNo z' z'' Hz'1 Hz''1) (SNo_mul_SNo z''' y Hz'''1 Hy1) (SNo_mul_SNo x w' Hx1 Hw'1) (SNo_mul_SNo z''' w' Hz'''1 Hw'1) to the current goal.
We will prove z' * y + x * z'' + z''' * w' < z''' * y + x * w' + z' * z''.
Apply SNoLt_tra (z' * y + x * z'' + z''' * w') (z''' * w' + z' * z'' + x * y) (z''' * y + x * w' + z' * z'') (SNo_add_SNo_3 (z' * y) (x * z'') (z''' * w') (SNo_mul_SNo z' y Hz'1 Hy1) (SNo_mul_SNo x z'' Hx1 Hz''1) (SNo_mul_SNo z''' w' Hz'''1 Hw'1)) (SNo_add_SNo_3 (z''' * w') (z' * z'') (x * y) (SNo_mul_SNo z''' w' Hz'''1 Hw'1) (SNo_mul_SNo z' z'' Hz'1 Hz''1) (SNo_mul_SNo x y Hx1 Hy1)) (SNo_add_SNo_3 (z''' * y) (x * w') (z' * z'') (SNo_mul_SNo z''' y Hz'''1 Hy1) (SNo_mul_SNo x w' Hx1 Hw'1) (SNo_mul_SNo z' z'' Hz'1 Hz''1)) to the current goal.
We will prove z' * y + x * z'' + z''' * w' < z''' * w' + z' * z'' + x * y.
rewrite the current goal using add_SNo_rotate_3_1 (z' * y) (x * z'') (z''' * w') (SNo_mul_SNo z' y Hz'1 Hy1) (SNo_mul_SNo x z'' Hx1 Hz''1) (SNo_mul_SNo z''' w' Hz'''1 Hw'1) (from left to right).
rewrite the current goal using add_SNo_com (z' * y) (x * z'') (SNo_mul_SNo z' y Hz'1 Hy1) (SNo_mul_SNo x z'' Hx1 Hz''1) (from left to right).
We will prove z''' * w' + x * z'' + z' * y < z''' * w' + z' * z'' + x * y.
Apply add_SNo_Lt2 (z''' * w') (x * z'' + z' * y) (z' * z'' + x * y) (SNo_mul_SNo z''' w' Hz'''1 Hw'1) (SNo_add_SNo (x * z'') (z' * y) (SNo_mul_SNo x z'' Hx1 Hz''1) (SNo_mul_SNo z' y Hz'1 Hy1)) (SNo_add_SNo (z' * z'') (x * y) (SNo_mul_SNo z' z'' Hz'1 Hz''1) (SNo_mul_SNo x y Hx1 Hy1)) to the current goal.
We will prove x * z'' + z' * y < z' * z'' + x * y.
An exact proof term for the current goal is mul_SNo_Lt z' z'' x y Hz'1 Hz''1 Hx1 Hy1 Hz'2 Hz''2.
We will prove z''' * w' + z' * z'' + x * y < z''' * y + x * w' + z' * z''.
rewrite the current goal using add_SNo_com_3_0_1 (z''' * w') (z' * z'') (x * y) (SNo_mul_SNo z''' w' Hz'''1 Hw'1) (SNo_mul_SNo z' z'' Hz'1 Hz''1) (SNo_mul_SNo x y Hx1 Hy1) (from left to right).
rewrite the current goal using add_SNo_rotate_3_1 (z''' * y) (x * w') (z' * z'') (SNo_mul_SNo z''' y Hz'''1 Hy1) (SNo_mul_SNo x w' Hx1 Hw'1) (SNo_mul_SNo z' z'' Hz'1 Hz''1) (from left to right).
We will prove z' * z'' + z''' * w' + x * y < z' * z'' + z''' * y + x * w'.
Apply add_SNo_Lt2 (z' * z'') (z''' * w' + x * y) (z''' * y + x * w') (SNo_mul_SNo z' z'' Hz'1 Hz''1) (SNo_add_SNo (z''' * w') (x * y) (SNo_mul_SNo z''' w' Hz'''1 Hw'1) (SNo_mul_SNo x y Hx1 Hy1)) (SNo_add_SNo (z''' * y) (x * w') (SNo_mul_SNo z''' y Hz'''1 Hy1) (SNo_mul_SNo x w' Hx1 Hw'1)) to the current goal.
We will prove z''' * w' + x * y < z''' * y + x * w'.
rewrite the current goal using add_SNo_com (z''' * w') (x * y) (SNo_mul_SNo z''' w' Hz'''1 Hw'1) (SNo_mul_SNo x y Hx1 Hy1) (from left to right).
An exact proof term for the current goal is mul_SNo_Lt z''' y x w' Hz'''1 Hy1 Hx1 Hw'1 Hz'''2 Hw'2.
We prove the intermediate claim Lxyeq: x * y = SNoCut (LxLy' ∪ RxRy') (LxRy' ∪ RxLy').
Set v to be the term SNoCut (LxLy' ∪ RxRy') (LxRy' ∪ RxLy').
Apply SNoCutP_SNoCut_impred (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') L1 to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ ordsucc ((⋃w ∈ LxLy' ∪ RxRy'ordsucc (SNoLev w)) ∪ (⋃z ∈ LxRy' ∪ RxLy'ordsucc (SNoLev z))).
Assume Hv3: ∀w ∈ LxLy' ∪ RxRy', w < v.
Assume Hv4: ∀z ∈ LxRy' ∪ RxLy', v < z.
Assume Hv5: ∀u, SNo u → (∀w ∈ LxLy' ∪ RxRy', w < u) → (∀z ∈ LxRy' ∪ RxLy', u < z) → SNoLev v ⊆ SNoLev u ∧ SNoEq_ (SNoLev v) v u.
Apply mul_SNo_eq_3 x y Hx1 Hy1 to the current goal.
Let L' and R' be given.
Assume HLR': SNoCutP L' R'.
Assume HL'E: ∀u, u ∈ L' → ∀q : prop, (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, u = z0 * y + x * z1 + - z0 * z1 → q) → q.
Assume HL'I1: ∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, w0 * y + x * w1 + - w0 * w1 ∈ L'.
Assume HL'I2: ∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, z0 * y + x * z1 + - z0 * z1 ∈ L'.
Assume HR'E: ∀u, u ∈ R' → ∀q : prop, (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, u = w0 * y + x * z1 + - w0 * z1 → q) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, u = z0 * y + x * w1 + - z0 * w1 → q) → q.
Assume HR'I1: ∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, w0 * y + x * z1 + - w0 * z1 ∈ R'.
Assume HR'I2: ∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, z0 * y + x * w1 + - z0 * w1 ∈ R'.
Assume HLR'eq: x * y = SNoCut L' R'.
rewrite the current goal using HLR'eq (from left to right).
Apply SNoCut_ext L' R' (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') to the current goal.
An exact proof term for the current goal is HLR'.
An exact proof term for the current goal is L1.
We will prove ∀w ∈ L', w < v.
Let w be given.
Assume Hw.
Apply HL'E w Hw to the current goal.
Let w0 be given.
Assume Hw0: w0 ∈ SNoL x.
Let w1 be given.
Assume Hw1: w1 ∈ SNoL y.
Assume Hwe.
rewrite the current goal using Hwe (from left to right).
We will prove w0 * y + x * w1 + - w0 * w1 < v.
Apply SNoL_E x Hx1 w0 Hw0 to the current goal.
Assume Hw0a Hw0b Hw0c.
Apply SNoL_E y Hy1 w1 Hw1 to the current goal.
Assume Hw1a Hw1b Hw1c.
We prove the intermediate claim L2: ∃w0' ∈ Lx, w0 ≤ w0'.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L2a: SNoLev x ⊆ SNoLev w0 ∧ SNoEq_ (SNoLev x) x w0.
Apply Hx5 w0 Hw0a to the current goal.
We will prove ∀w' ∈ Lx, w' < w0.
Let w' be given.
Assume Hw'.
Apply SNoLtLe_or w' w0 (HLRx1 w' Hw') Hw0a to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume H: w0 ≤ w'.
We will prove False.
Apply HC to the current goal.
We use w' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw'.
We will prove w0 ≤ w'.
An exact proof term for the current goal is H.
We will prove ∀z' ∈ Rx, w0 < z'.
Let z' be given.
Assume Hz'.
Apply SNoLt_tra w0 x z' Hw0a Hx1 (HLRx2 z' Hz') to the current goal.
We will prove w0 < x.
An exact proof term for the current goal is Hw0c.
We will prove x < z'.
An exact proof term for the current goal is Hx4 z' Hz'.
Apply L2a to the current goal.
Assume Hxw0: SNoLev x ⊆ SNoLev w0.
Assume _.
Apply In_irref (SNoLev w0) to the current goal.
We will prove SNoLev w0 ∈ SNoLev w0.
Apply Hxw0 to the current goal.
An exact proof term for the current goal is Hw0b.
We prove the intermediate claim L3: ∃w1' ∈ Ly, w1 ≤ w1'.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L3a: SNoLev y ⊆ SNoLev w1 ∧ SNoEq_ (SNoLev y) y w1.
Apply Hy5 w1 Hw1a to the current goal.
We will prove ∀w' ∈ Ly, w' < w1.
Let w' be given.
Assume Hw'.
Apply SNoLtLe_or w' w1 (HLRy1 w' Hw') Hw1a to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume H: w1 ≤ w'.
We will prove False.
Apply HC to the current goal.
We use w' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw'.
We will prove w1 ≤ w'.
An exact proof term for the current goal is H.
We will prove ∀z' ∈ Ry, w1 < z'.
Let z' be given.
Assume Hz'.
Apply SNoLt_tra w1 y z' Hw1a Hy1 (HLRy2 z' Hz') to the current goal.
We will prove w1 < y.
An exact proof term for the current goal is Hw1c.
We will prove y < z'.
An exact proof term for the current goal is Hy4 z' Hz'.
Apply L3a to the current goal.
Assume Hyw1: SNoLev y ⊆ SNoLev w1.
Assume _.
Apply In_irref (SNoLev w1) to the current goal.
We will prove SNoLev w1 ∈ SNoLev w1.
Apply Hyw1 to the current goal.
An exact proof term for the current goal is Hw1b.
Apply L2 to the current goal.
Let w0' be given.
Assume H.
Apply H to the current goal.
Assume Hw0'1: w0' ∈ Lx.
Assume Hw0'2: w0 ≤ w0'.
Apply L3 to the current goal.
Let w1' be given.
Assume H.
Apply H to the current goal.
Assume Hw1'1: w1' ∈ Ly.
Assume Hw1'2: w1 ≤ w1'.
We will prove w0 * y + x * w1 + - w0 * w1 < v.
Apply SNoLeLt_tra (w0 * y + x * w1 + - w0 * w1) (w0' * y + x * w1' + - w0' * w1') v (SNo_add_SNo_3 (w0 * y) (x * w1) (- w0 * w1) (SNo_mul_SNo w0 y Hw0a Hy1) (SNo_mul_SNo x w1 Hx1 Hw1a) (SNo_minus_SNo (w0 * w1) (SNo_mul_SNo w0 w1 Hw0a Hw1a))) (SNo_add_SNo_3 (w0' * y) (x * w1') (- w0' * w1') (SNo_mul_SNo w0' y (HLRx1 w0' Hw0'1) Hy1) (SNo_mul_SNo x w1' Hx1 (HLRy1 w1' Hw1'1)) (SNo_minus_SNo (w0' * w1') (SNo_mul_SNo w0' w1' (HLRx1 w0' Hw0'1) (HLRy1 w1' Hw1'1)))) Hv1 to the current goal.
We will prove w0 * y + x * w1 + - w0 * w1 ≤ w0' * y + x * w1' + - w0' * w1'.
Apply add_SNo_minus_Le12b3 (w0 * y) (x * w1) (w0 * w1) (w0' * y) (x * w1') (w0' * w1') (SNo_mul_SNo w0 y Hw0a Hy1) (SNo_mul_SNo x w1 Hx1 Hw1a) (SNo_mul_SNo w0 w1 Hw0a Hw1a) (SNo_mul_SNo w0' y (HLRx1 w0' Hw0'1) Hy1) (SNo_mul_SNo x w1' Hx1 (HLRy1 w1' Hw1'1)) (SNo_mul_SNo w0' w1' (HLRx1 w0' Hw0'1) (HLRy1 w1' Hw1'1)) to the current goal.
We will prove w0 * y + x * w1 + w0' * w1' ≤ w0' * y + x * w1' + w0 * w1.
Apply SNoLe_tra (w0 * y + x * w1 + w0' * w1') (w0 * y + x * w1' + w0' * w1) (w0' * y + x * w1' + w0 * w1) (SNo_add_SNo_3 (w0 * y) (x * w1) (w0' * w1') (SNo_mul_SNo w0 y Hw0a Hy1) (SNo_mul_SNo x w1 Hx1 Hw1a) (SNo_mul_SNo w0' w1' (HLRx1 w0' Hw0'1) (HLRy1 w1' Hw1'1))) (SNo_add_SNo_3 (w0 * y) (x * w1') (w0' * w1) (SNo_mul_SNo w0 y Hw0a Hy1) (SNo_mul_SNo x w1' Hx1 (HLRy1 w1' Hw1'1)) (SNo_mul_SNo w0' w1 (HLRx1 w0' Hw0'1) Hw1a)) (SNo_add_SNo_3 (w0' * y) (x * w1') (w0 * w1) (SNo_mul_SNo w0' y (HLRx1 w0' Hw0'1) Hy1) (SNo_mul_SNo x w1' Hx1 (HLRy1 w1' Hw1'1)) (SNo_mul_SNo w0 w1 Hw0a Hw1a)) to the current goal.
We will prove w0 * y + x * w1 + w0' * w1' ≤ w0 * y + x * w1' + w0' * w1.
Apply add_SNo_Le2 (w0 * y) (x * w1 + w0' * w1') (x * w1' + w0' * w1) (SNo_mul_SNo w0 y Hw0a Hy1) (SNo_add_SNo (x * w1) (w0' * w1') (SNo_mul_SNo x w1 Hx1 Hw1a) (SNo_mul_SNo w0' w1' (HLRx1 w0' Hw0'1) (HLRy1 w1' Hw1'1))) (SNo_add_SNo (x * w1') (w0' * w1) (SNo_mul_SNo x w1' Hx1 (HLRy1 w1' Hw1'1)) (SNo_mul_SNo w0' w1 (HLRx1 w0' Hw0'1) Hw1a)) to the current goal.
We will prove x * w1 + w0' * w1' ≤ x * w1' + w0' * w1.
rewrite the current goal using add_SNo_com (x * w1) (w0' * w1') (SNo_mul_SNo x w1 Hx1 Hw1a) (SNo_mul_SNo w0' w1' (HLRx1 w0' Hw0'1) (HLRy1 w1' Hw1'1)) (from left to right).
We will prove w0' * w1' + x * w1 ≤ x * w1' + w0' * w1.
Apply mul_SNo_Le x w1' w0' w1 Hx1 (HLRy1 w1' Hw1'1) (HLRx1 w0' Hw0'1) Hw1a to the current goal.
We will prove w0' ≤ x.
Apply SNoLtLe to the current goal.
We will prove w0' < x.
An exact proof term for the current goal is Hx3 w0' Hw0'1.
We will prove w1 ≤ w1'.
An exact proof term for the current goal is Hw1'2.
We will prove w0 * y + x * w1' + w0' * w1 ≤ w0' * y + x * w1' + w0 * w1.
rewrite the current goal using add_SNo_com_3_0_1 (w0 * y) (x * w1') (w0' * w1) (SNo_mul_SNo w0 y Hw0a Hy1) (SNo_mul_SNo x w1' Hx1 (HLRy1 w1' Hw1'1)) (SNo_mul_SNo w0' w1 (HLRx1 w0' Hw0'1) Hw1a) (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (w0' * y) (x * w1') (w0 * w1) (SNo_mul_SNo w0' y (HLRx1 w0' Hw0'1) Hy1) (SNo_mul_SNo x w1' Hx1 (HLRy1 w1' Hw1'1)) (SNo_mul_SNo w0 w1 Hw0a Hw1a) (from left to right).
Apply add_SNo_Le2 (x * w1') (w0 * y + w0' * w1) (w0' * y + w0 * w1) (SNo_mul_SNo x w1' Hx1 (HLRy1 w1' Hw1'1)) (SNo_add_SNo (w0 * y) (w0' * w1) (SNo_mul_SNo w0 y Hw0a Hy1) (SNo_mul_SNo w0' w1 (HLRx1 w0' Hw0'1) Hw1a)) (SNo_add_SNo (w0' * y) (w0 * w1) (SNo_mul_SNo w0' y (HLRx1 w0' Hw0'1) Hy1) (SNo_mul_SNo w0 w1 Hw0a Hw1a)) to the current goal.
We will prove w0 * y + w0' * w1 ≤ w0' * y + w0 * w1.
Apply mul_SNo_Le w0' y w0 w1 (HLRx1 w0' Hw0'1) Hy1 Hw0a Hw1a to the current goal.
We will prove w0 ≤ w0'.
An exact proof term for the current goal is Hw0'2.
We will prove w1 ≤ y.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hw1c.
We will prove w0' * y + x * w1' + - w0' * w1' < v.
Apply Hv3 to the current goal.
We will prove w0' * y + x * w1' + - w0' * w1' ∈ LxLy' ∪ RxRy'.
Apply binunionI1 to the current goal.
Apply LxLy'I to the current goal.
An exact proof term for the current goal is Hw0'1.
An exact proof term for the current goal is Hw1'1.
Let z0 be given.
Assume Hz0: z0 ∈ SNoR x.
Let z1 be given.
Assume Hz1: z1 ∈ SNoR y.
Assume Hwe.
rewrite the current goal using Hwe (from left to right).
We will prove z0 * y + x * z1 + - z0 * z1 < v.
Apply SNoR_E x Hx1 z0 Hz0 to the current goal.
Assume Hz0a Hz0b Hz0c.
Apply SNoR_E y Hy1 z1 Hz1 to the current goal.
Assume Hz1a Hz1b Hz1c.
We prove the intermediate claim L4: ∃z0' ∈ Rx, z0' ≤ z0.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L4a: SNoLev x ⊆ SNoLev z0 ∧ SNoEq_ (SNoLev x) x z0.
Apply Hx5 z0 Hz0a to the current goal.
We will prove ∀w' ∈ Lx, w' < z0.
Let w' be given.
Assume Hw'.
Apply SNoLt_tra w' x z0 (HLRx1 w' Hw') Hx1 Hz0a to the current goal.
We will prove w' < x.
An exact proof term for the current goal is Hx3 w' Hw'.
We will prove x < z0.
An exact proof term for the current goal is Hz0c.
We will prove ∀z' ∈ Rx, z0 < z'.
Let z' be given.
Assume Hz'.
Apply SNoLtLe_or z0 z' Hz0a (HLRx2 z' Hz') to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume H: z' ≤ z0.
We will prove False.
Apply HC to the current goal.
We use z' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz'.
We will prove z' ≤ z0.
An exact proof term for the current goal is H.
Apply L4a to the current goal.
Assume Hxz0: SNoLev x ⊆ SNoLev z0.
Assume _.
Apply In_irref (SNoLev z0) to the current goal.
We will prove SNoLev z0 ∈ SNoLev z0.
Apply Hxz0 to the current goal.
An exact proof term for the current goal is Hz0b.
We prove the intermediate claim L5: ∃z1' ∈ Ry, z1' ≤ z1.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L5a: SNoLev y ⊆ SNoLev z1 ∧ SNoEq_ (SNoLev y) y z1.
Apply Hy5 z1 Hz1a to the current goal.
We will prove ∀w' ∈ Ly, w' < z1.
Let w' be given.
Assume Hw'.
Apply SNoLt_tra w' y z1 (HLRy1 w' Hw') Hy1 Hz1a to the current goal.
We will prove w' < y.
An exact proof term for the current goal is Hy3 w' Hw'.
We will prove y < z1.
An exact proof term for the current goal is Hz1c.
We will prove ∀z' ∈ Ry, z1 < z'.
Let z' be given.
Assume Hz'.
Apply SNoLtLe_or z1 z' Hz1a (HLRy2 z' Hz') to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume H: z' ≤ z1.
We will prove False.
Apply HC to the current goal.
We use z' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz'.
We will prove z' ≤ z1.
An exact proof term for the current goal is H.
Apply L5a to the current goal.
Assume Hyz1: SNoLev y ⊆ SNoLev z1.
Assume _.
Apply In_irref (SNoLev z1) to the current goal.
We will prove SNoLev z1 ∈ SNoLev z1.
Apply Hyz1 to the current goal.
An exact proof term for the current goal is Hz1b.
Apply L4 to the current goal.
Let z0' be given.
Assume H.
Apply H to the current goal.
Assume Hz0'1: z0' ∈ Rx.
Assume Hz0'2: z0' ≤ z0.
Apply L5 to the current goal.
Let z1' be given.
Assume H.
Apply H to the current goal.
Assume Hz1'1: z1' ∈ Ry.
Assume Hz1'2: z1' ≤ z1.
We will prove z0 * y + x * z1 + - z0 * z1 < v.
Apply SNoLeLt_tra (z0 * y + x * z1 + - z0 * z1) (z0' * y + x * z1' + - z0' * z1') v (SNo_add_SNo_3 (z0 * y) (x * z1) (- z0 * z1) (SNo_mul_SNo z0 y Hz0a Hy1) (SNo_mul_SNo x z1 Hx1 Hz1a) (SNo_minus_SNo (z0 * z1) (SNo_mul_SNo z0 z1 Hz0a Hz1a))) (SNo_add_SNo_3 (z0' * y) (x * z1') (- z0' * z1') (SNo_mul_SNo z0' y (HLRx2 z0' Hz0'1) Hy1) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1)) (SNo_minus_SNo (z0' * z1') (SNo_mul_SNo z0' z1' (HLRx2 z0' Hz0'1) (HLRy2 z1' Hz1'1)))) Hv1 to the current goal.
We will prove z0 * y + x * z1 + - z0 * z1 ≤ z0' * y + x * z1' + - z0' * z1'.
Apply add_SNo_minus_Le12b3 (z0 * y) (x * z1) (z0 * z1) (z0' * y) (x * z1') (z0' * z1') (SNo_mul_SNo z0 y Hz0a Hy1) (SNo_mul_SNo x z1 Hx1 Hz1a) (SNo_mul_SNo z0 z1 Hz0a Hz1a) (SNo_mul_SNo z0' y (HLRx2 z0' Hz0'1) Hy1) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1)) (SNo_mul_SNo z0' z1' (HLRx2 z0' Hz0'1) (HLRy2 z1' Hz1'1)) to the current goal.
We will prove z0 * y + x * z1 + z0' * z1' ≤ z0' * y + x * z1' + z0 * z1.
Apply SNoLe_tra (z0 * y + x * z1 + z0' * z1') (z0 * y + z0' * z1 + x * z1') (z0' * y + x * z1' + z0 * z1) (SNo_add_SNo_3 (z0 * y) (x * z1) (z0' * z1') (SNo_mul_SNo z0 y Hz0a Hy1) (SNo_mul_SNo x z1 Hx1 Hz1a) (SNo_mul_SNo z0' z1' (HLRx2 z0' Hz0'1) (HLRy2 z1' Hz1'1))) (SNo_add_SNo_3 (z0 * y) (z0' * z1) (x * z1') (SNo_mul_SNo z0 y Hz0a Hy1) (SNo_mul_SNo z0' z1 (HLRx2 z0' Hz0'1) Hz1a) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1))) (SNo_add_SNo_3 (z0' * y) (x * z1') (z0 * z1) (SNo_mul_SNo z0' y (HLRx2 z0' Hz0'1) Hy1) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1)) (SNo_mul_SNo z0 z1 Hz0a Hz1a)) to the current goal.
We will prove z0 * y + x * z1 + z0' * z1' ≤ z0 * y + z0' * z1 + x * z1'.
Apply add_SNo_Le2 (z0 * y) (x * z1 + z0' * z1') (z0' * z1 + x * z1') (SNo_mul_SNo z0 y Hz0a Hy1) (SNo_add_SNo (x * z1) (z0' * z1') (SNo_mul_SNo x z1 Hx1 Hz1a) (SNo_mul_SNo z0' z1' (HLRx2 z0' Hz0'1) (HLRy2 z1' Hz1'1))) (SNo_add_SNo (z0' * z1) (x * z1') (SNo_mul_SNo z0' z1 (HLRx2 z0' Hz0'1) Hz1a) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1))) to the current goal.
We will prove x * z1 + z0' * z1' ≤ z0' * z1 + x * z1'.
Apply mul_SNo_Le z0' z1 x z1' (HLRx2 z0' Hz0'1) Hz1a Hx1 (HLRy2 z1' Hz1'1) to the current goal.
We will prove x ≤ z0'.
Apply SNoLtLe to the current goal.
We will prove x < z0'.
An exact proof term for the current goal is Hx4 z0' Hz0'1.
We will prove z1' ≤ z1.
An exact proof term for the current goal is Hz1'2.
We will prove z0 * y + z0' * z1 + x * z1' ≤ z0' * y + x * z1' + z0 * z1.
rewrite the current goal using add_SNo_rotate_3_1 (z0 * y) (z0' * z1) (x * z1') (SNo_mul_SNo z0 y Hz0a Hy1) (SNo_mul_SNo z0' z1 (HLRx2 z0' Hz0'1) Hz1a) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1)) (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (z0' * y) (x * z1') (z0 * z1) (SNo_mul_SNo z0' y (HLRx2 z0' Hz0'1) Hy1) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1)) (SNo_mul_SNo z0 z1 Hz0a Hz1a) (from left to right).
We will prove x * z1' + z0 * y + z0' * z1 ≤ x * z1' + z0' * y + z0 * z1.
Apply add_SNo_Le2 (x * z1') (z0 * y + z0' * z1) (z0' * y + z0 * z1) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1)) (SNo_add_SNo (z0 * y) (z0' * z1) (SNo_mul_SNo z0 y Hz0a Hy1) (SNo_mul_SNo z0' z1 (HLRx2 z0' Hz0'1) Hz1a)) (SNo_add_SNo (z0' * y) (z0 * z1) (SNo_mul_SNo z0' y (HLRx2 z0' Hz0'1) Hy1) (SNo_mul_SNo z0 z1 Hz0a Hz1a)) to the current goal.
We will prove z0 * y + z0' * z1 ≤ z0' * y + z0 * z1.
rewrite the current goal using add_SNo_com (z0 * y) (z0' * z1) (SNo_mul_SNo z0 y Hz0a Hy1) (SNo_mul_SNo z0' z1 (HLRx2 z0' Hz0'1) Hz1a) (from left to right).
rewrite the current goal using add_SNo_com (z0' * y) (z0 * z1) (SNo_mul_SNo z0' y (HLRx2 z0' Hz0'1) Hy1) (SNo_mul_SNo z0 z1 Hz0a Hz1a) (from left to right).
Apply mul_SNo_Le z0 z1 z0' y Hz0a Hz1a (HLRx2 z0' Hz0'1) Hy1 to the current goal.
We will prove z0' ≤ z0.
An exact proof term for the current goal is Hz0'2.
We will prove y ≤ z1.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hz1c.
We will prove z0' * y + x * z1' + - z0' * z1' < v.
Apply Hv3 to the current goal.
We will prove z0' * y + x * z1' + - z0' * z1' ∈ LxLy' ∪ RxRy'.
Apply binunionI2 to the current goal.
Apply RxRy'I to the current goal.
An exact proof term for the current goal is Hz0'1.
An exact proof term for the current goal is Hz1'1.
We will prove ∀z ∈ R', v < z.
Let z be given.
Assume Hz.
Apply HR'E z Hz to the current goal.
Let w0 be given.
Assume Hw0: w0 ∈ SNoL x.
Let z1 be given.
Assume Hz1: z1 ∈ SNoR y.
Assume Hze.
rewrite the current goal using Hze (from left to right).
We will prove v < w0 * y + x * z1 + - w0 * z1.
Apply SNoL_E x Hx1 w0 Hw0 to the current goal.
Assume Hw0a Hw0b Hw0c.
Apply SNoR_E y Hy1 z1 Hz1 to the current goal.
Assume Hz1a Hz1b Hz1c.
We prove the intermediate claim L6: ∃w0' ∈ Lx, w0 ≤ w0'.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L6a: SNoLev x ⊆ SNoLev w0 ∧ SNoEq_ (SNoLev x) x w0.
Apply Hx5 w0 Hw0a to the current goal.
We will prove ∀w' ∈ Lx, w' < w0.
Let w' be given.
Assume Hw'.
Apply SNoLtLe_or w' w0 (HLRx1 w' Hw') Hw0a to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume H: w0 ≤ w'.
We will prove False.
Apply HC to the current goal.
We use w' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw'.
We will prove w0 ≤ w'.
An exact proof term for the current goal is H.
We will prove ∀z' ∈ Rx, w0 < z'.
Let z' be given.
Assume Hz'.
Apply SNoLt_tra w0 x z' Hw0a Hx1 (HLRx2 z' Hz') to the current goal.
We will prove w0 < x.
An exact proof term for the current goal is Hw0c.
We will prove x < z'.
An exact proof term for the current goal is Hx4 z' Hz'.
Apply L6a to the current goal.
Assume Hxw0: SNoLev x ⊆ SNoLev w0.
Assume _.
Apply In_irref (SNoLev w0) to the current goal.
We will prove SNoLev w0 ∈ SNoLev w0.
Apply Hxw0 to the current goal.
An exact proof term for the current goal is Hw0b.
We prove the intermediate claim L7: ∃z1' ∈ Ry, z1' ≤ z1.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L7a: SNoLev y ⊆ SNoLev z1 ∧ SNoEq_ (SNoLev y) y z1.
Apply Hy5 z1 Hz1a to the current goal.
We will prove ∀w' ∈ Ly, w' < z1.
Let w' be given.
Assume Hw'.
Apply SNoLt_tra w' y z1 (HLRy1 w' Hw') Hy1 Hz1a to the current goal.
We will prove w' < y.
An exact proof term for the current goal is Hy3 w' Hw'.
We will prove y < z1.
An exact proof term for the current goal is Hz1c.
We will prove ∀z' ∈ Ry, z1 < z'.
Let z' be given.
Assume Hz'.
Apply SNoLtLe_or z1 z' Hz1a (HLRy2 z' Hz') to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume H: z' ≤ z1.
We will prove False.
Apply HC to the current goal.
We use z' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz'.
We will prove z' ≤ z1.
An exact proof term for the current goal is H.
Apply L7a to the current goal.
Assume Hyz1: SNoLev y ⊆ SNoLev z1.
Assume _.
Apply In_irref (SNoLev z1) to the current goal.
We will prove SNoLev z1 ∈ SNoLev z1.
Apply Hyz1 to the current goal.
An exact proof term for the current goal is Hz1b.
Apply L6 to the current goal.
Let w0' be given.
Assume H.
Apply H to the current goal.
Assume Hw0'1: w0' ∈ Lx.
Assume Hw0'2: w0 ≤ w0'.
Apply L7 to the current goal.
Let z1' be given.
Assume H.
Apply H to the current goal.
Assume Hz1'1: z1' ∈ Ry.
Assume Hz1'2: z1' ≤ z1.
We will prove v < w0 * y + x * z1 + - w0 * z1.
Apply SNoLtLe_tra v (w0' * y + x * z1' + - w0' * z1') (w0 * y + x * z1 + - w0 * z1) Hv1 (SNo_add_SNo_3 (w0' * y) (x * z1') (- w0' * z1') (SNo_mul_SNo w0' y (HLRx1 w0' Hw0'1) Hy1) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1)) (SNo_minus_SNo (w0' * z1') (SNo_mul_SNo w0' z1' (HLRx1 w0' Hw0'1) (HLRy2 z1' Hz1'1)))) (SNo_add_SNo_3 (w0 * y) (x * z1) (- w0 * z1) (SNo_mul_SNo w0 y Hw0a Hy1) (SNo_mul_SNo x z1 Hx1 Hz1a) (SNo_minus_SNo (w0 * z1) (SNo_mul_SNo w0 z1 Hw0a Hz1a))) to the current goal.
We will prove v < w0' * y + x * z1' + - w0' * z1'.
Apply Hv4 to the current goal.
We will prove w0' * y + x * z1' + - w0' * z1' ∈ LxRy' ∪ RxLy'.
Apply binunionI1 to the current goal.
Apply LxRy'I to the current goal.
An exact proof term for the current goal is Hw0'1.
An exact proof term for the current goal is Hz1'1.
We will prove w0' * y + x * z1' + - w0' * z1' ≤ w0 * y + x * z1 + - w0 * z1.
Apply add_SNo_minus_Le12b3 (w0' * y) (x * z1') (w0' * z1') (w0 * y) (x * z1) (w0 * z1) (SNo_mul_SNo w0' y (HLRx1 w0' Hw0'1) Hy1) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1)) (SNo_mul_SNo w0' z1' (HLRx1 w0' Hw0'1) (HLRy2 z1' Hz1'1)) (SNo_mul_SNo w0 y Hw0a Hy1) (SNo_mul_SNo x z1 Hx1 Hz1a) (SNo_mul_SNo w0 z1 Hw0a Hz1a) to the current goal.
We will prove w0' * y + x * z1' + w0 * z1 ≤ w0 * y + x * z1 + w0' * z1'.
Apply SNoLe_tra (w0' * y + x * z1' + w0 * z1) (x * z1' + w0' * z1 + w0 * y) (w0 * y + x * z1 + w0' * z1') (SNo_add_SNo_3 (w0' * y) (x * z1') (w0 * z1) (SNo_mul_SNo w0' y (HLRx1 w0' Hw0'1) Hy1) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1)) (SNo_mul_SNo w0 z1 Hw0a Hz1a)) (SNo_add_SNo_3 (x * z1') (w0' * z1) (w0 * y) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1)) (SNo_mul_SNo w0' z1 (HLRx1 w0' Hw0'1) Hz1a) (SNo_mul_SNo w0 y Hw0a Hy1)) (SNo_add_SNo_3 (w0 * y) (x * z1) (w0' * z1') (SNo_mul_SNo w0 y Hw0a Hy1) (SNo_mul_SNo x z1 Hx1 Hz1a) (SNo_mul_SNo w0' z1' (HLRx1 w0' Hw0'1) (HLRy2 z1' Hz1'1))) to the current goal.
We will prove w0' * y + x * z1' + w0 * z1 ≤ x * z1' + w0' * z1 + w0 * y.
rewrite the current goal using add_SNo_com_3_0_1 (w0' * y) (x * z1') (w0 * z1) (SNo_mul_SNo w0' y (HLRx1 w0' Hw0'1) Hy1) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1)) (SNo_mul_SNo w0 z1 Hw0a Hz1a) (from left to right).
Apply add_SNo_Le2 (x * z1') (w0' * y + w0 * z1) (w0' * z1 + w0 * y) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1)) (SNo_add_SNo (w0' * y) (w0 * z1) (SNo_mul_SNo w0' y (HLRx1 w0' Hw0'1) Hy1) (SNo_mul_SNo w0 z1 Hw0a Hz1a)) (SNo_add_SNo (w0' * z1) (w0 * y) (SNo_mul_SNo w0' z1 (HLRx1 w0' Hw0'1) Hz1a) (SNo_mul_SNo w0 y Hw0a Hy1)) to the current goal.
We will prove w0' * y + w0 * z1 ≤ w0' * z1 + w0 * y.
rewrite the current goal using add_SNo_com (w0' * y) (w0 * z1) (SNo_mul_SNo w0' y (HLRx1 w0' Hw0'1) Hy1) (SNo_mul_SNo w0 z1 Hw0a Hz1a) (from left to right).
Apply mul_SNo_Le w0' z1 w0 y (HLRx1 w0' Hw0'1) Hz1a Hw0a Hy1 to the current goal.
We will prove w0 ≤ w0'.
An exact proof term for the current goal is Hw0'2.
We will prove y ≤ z1.
Apply SNoLtLe to the current goal.
We will prove y < z1.
An exact proof term for the current goal is Hz1c.
We will prove x * z1' + w0' * z1 + w0 * y ≤ w0 * y + x * z1 + w0' * z1'.
rewrite the current goal using add_SNo_rotate_3_1 (x * z1') (w0' * z1) (w0 * y) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1)) (SNo_mul_SNo w0' z1 (HLRx1 w0' Hw0'1) Hz1a) (SNo_mul_SNo w0 y Hw0a Hy1) (from left to right).
We will prove w0 * y + x * z1' + w0' * z1 ≤ w0 * y + x * z1 + w0' * z1'.
Apply add_SNo_Le2 (w0 * y) (x * z1' + w0' * z1) (x * z1 + w0' * z1') (SNo_mul_SNo w0 y Hw0a Hy1) (SNo_add_SNo (x * z1') (w0' * z1) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1)) (SNo_mul_SNo w0' z1 (HLRx1 w0' Hw0'1) Hz1a)) (SNo_add_SNo (x * z1) (w0' * z1') (SNo_mul_SNo x z1 Hx1 Hz1a) (SNo_mul_SNo w0' z1' (HLRx1 w0' Hw0'1) (HLRy2 z1' Hz1'1))) to the current goal.
We will prove x * z1' + w0' * z1 ≤ x * z1 + w0' * z1'.
rewrite the current goal using add_SNo_com (x * z1') (w0' * z1) (SNo_mul_SNo x z1' Hx1 (HLRy2 z1' Hz1'1)) (SNo_mul_SNo w0' z1 (HLRx1 w0' Hw0'1) Hz1a) (from left to right).
We will prove w0' * z1 + x * z1' ≤ x * z1 + w0' * z1'.
Apply mul_SNo_Le x z1 w0' z1' Hx1 Hz1a (HLRx1 w0' Hw0'1) (HLRy2 z1' Hz1'1) to the current goal.
We will prove w0' ≤ x.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hx3 w0' Hw0'1.
We will prove z1' ≤ z1.
An exact proof term for the current goal is Hz1'2.
Let z0 be given.
Assume Hz0: z0 ∈ SNoR x.
Let w1 be given.
Assume Hw1: w1 ∈ SNoL y.
Assume Hze.
rewrite the current goal using Hze (from left to right).
We will prove v < z0 * y + x * w1 + - z0 * w1.
Apply SNoR_E x Hx1 z0 Hz0 to the current goal.
Assume Hz0a Hz0b Hz0c.
Apply SNoL_E y Hy1 w1 Hw1 to the current goal.
Assume Hw1a Hw1b Hw1c.
We prove the intermediate claim L8: ∃z0' ∈ Rx, z0' ≤ z0.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L8a: SNoLev x ⊆ SNoLev z0 ∧ SNoEq_ (SNoLev x) x z0.
Apply Hx5 z0 Hz0a to the current goal.
We will prove ∀w' ∈ Lx, w' < z0.
Let w' be given.
Assume Hw'.
Apply SNoLt_tra w' x z0 (HLRx1 w' Hw') Hx1 Hz0a to the current goal.
We will prove w' < x.
An exact proof term for the current goal is Hx3 w' Hw'.
We will prove x < z0.
An exact proof term for the current goal is Hz0c.
We will prove ∀z' ∈ Rx, z0 < z'.
Let z' be given.
Assume Hz'.
Apply SNoLtLe_or z0 z' Hz0a (HLRx2 z' Hz') to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume H: z' ≤ z0.
We will prove False.
Apply HC to the current goal.
We use z' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz'.
We will prove z' ≤ z0.
An exact proof term for the current goal is H.
Apply L8a to the current goal.
Assume Hxz0: SNoLev x ⊆ SNoLev z0.
Assume _.
Apply In_irref (SNoLev z0) to the current goal.
We will prove SNoLev z0 ∈ SNoLev z0.
Apply Hxz0 to the current goal.
An exact proof term for the current goal is Hz0b.
We prove the intermediate claim L9: ∃w1' ∈ Ly, w1 ≤ w1'.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L9a: SNoLev y ⊆ SNoLev w1 ∧ SNoEq_ (SNoLev y) y w1.
Apply Hy5 w1 Hw1a to the current goal.
We will prove ∀w' ∈ Ly, w' < w1.
Let w' be given.
Assume Hw'.
Apply SNoLtLe_or w' w1 (HLRy1 w' Hw') Hw1a to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume H: w1 ≤ w'.
We will prove False.
Apply HC to the current goal.
We use w' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw'.
We will prove w1 ≤ w'.
An exact proof term for the current goal is H.
We will prove ∀z' ∈ Ry, w1 < z'.
Let z' be given.
Assume Hz'.
Apply SNoLt_tra w1 y z' Hw1a Hy1 (HLRy2 z' Hz') to the current goal.
We will prove w1 < y.
An exact proof term for the current goal is Hw1c.
We will prove y < z'.
An exact proof term for the current goal is Hy4 z' Hz'.
Apply L9a to the current goal.
Assume Hyw1: SNoLev y ⊆ SNoLev w1.
Assume _.
Apply In_irref (SNoLev w1) to the current goal.
We will prove SNoLev w1 ∈ SNoLev w1.
Apply Hyw1 to the current goal.
An exact proof term for the current goal is Hw1b.
Apply L8 to the current goal.
Let z0' be given.
Assume H.
Apply H to the current goal.
Assume Hz0'1: z0' ∈ Rx.
Assume Hz0'2: z0' ≤ z0.
Apply L9 to the current goal.
Let w1' be given.
Assume H.
Apply H to the current goal.
Assume Hw1'1: w1' ∈ Ly.
Assume Hw1'2: w1 ≤ w1'.
We will prove v < z0 * y + x * w1 + - z0 * w1.
Apply SNoLtLe_tra v (z0' * y + x * w1' + - z0' * w1') (z0 * y + x * w1 + - z0 * w1) Hv1 (SNo_add_SNo_3 (z0' * y) (x * w1') (- z0' * w1') (SNo_mul_SNo z0' y (HLRx2 z0' Hz0'1) Hy1) (SNo_mul_SNo x w1' Hx1 (HLRy1 w1' Hw1'1)) (SNo_minus_SNo (z0' * w1') (SNo_mul_SNo z0' w1' (HLRx2 z0' Hz0'1) (HLRy1 w1' Hw1'1)))) (SNo_add_SNo_3 (z0 * y) (x * w1) (- z0 * w1) (SNo_mul_SNo z0 y Hz0a Hy1) (SNo_mul_SNo x w1 Hx1 Hw1a) (SNo_minus_SNo (z0 * w1) (SNo_mul_SNo z0 w1 Hz0a Hw1a))) to the current goal.
We will prove v < z0' * y + x * w1' + - z0' * w1'.
Apply Hv4 to the current goal.
We will prove z0' * y + x * w1' + - z0' * w1' ∈ LxRy' ∪ RxLy'.
Apply binunionI2 to the current goal.
Apply RxLy'I to the current goal.
An exact proof term for the current goal is Hz0'1.
An exact proof term for the current goal is Hw1'1.
We will prove z0' * y + x * w1' + - z0' * w1' ≤ z0 * y + x * w1 + - z0 * w1.
Apply add_SNo_minus_Le12b3 (z0' * y) (x * w1') (z0' * w1') (z0 * y) (x * w1) (z0 * w1) (SNo_mul_SNo z0' y (HLRx2 z0' Hz0'1) Hy1) (SNo_mul_SNo x w1' Hx1 (HLRy1 w1' Hw1'1)) (SNo_mul_SNo z0' w1' (HLRx2 z0' Hz0'1) (HLRy1 w1' Hw1'1)) (SNo_mul_SNo z0 y Hz0a Hy1) (SNo_mul_SNo x w1 Hx1 Hw1a) (SNo_mul_SNo z0 w1 Hz0a Hw1a) to the current goal.
We will prove z0' * y + x * w1' + z0 * w1 ≤ z0 * y + x * w1 + z0' * w1'.
Apply SNoLe_tra (z0' * y + x * w1' + z0 * w1) (z0' * y + x * w1 + z0 * w1') (z0 * y + x * w1 + z0' * w1') (SNo_add_SNo_3 (z0' * y) (x * w1') (z0 * w1) (SNo_mul_SNo z0' y (HLRx2 z0' Hz0'1) Hy1) (SNo_mul_SNo x w1' Hx1 (HLRy1 w1' Hw1'1)) (SNo_mul_SNo z0 w1 Hz0a Hw1a)) (SNo_add_SNo_3 (z0' * y) (x * w1) (z0 * w1') (SNo_mul_SNo z0' y (HLRx2 z0' Hz0'1) Hy1) (SNo_mul_SNo x w1 Hx1 Hw1a) (SNo_mul_SNo z0 w1' Hz0a (HLRy1 w1' Hw1'1))) (SNo_add_SNo_3 (z0 * y) (x * w1) (z0' * w1') (SNo_mul_SNo z0 y Hz0a Hy1) (SNo_mul_SNo x w1 Hx1 Hw1a) (SNo_mul_SNo z0' w1' (HLRx2 z0' Hz0'1) (HLRy1 w1' Hw1'1))) to the current goal.
We will prove z0' * y + x * w1' + z0 * w1 ≤ z0' * y + x * w1 + z0 * w1'.
Apply add_SNo_Le2 (z0' * y) (x * w1' + z0 * w1) (x * w1 + z0 * w1') (SNo_mul_SNo z0' y (HLRx2 z0' Hz0'1) Hy1) (SNo_add_SNo (x * w1') (z0 * w1) (SNo_mul_SNo x w1' Hx1 (HLRy1 w1' Hw1'1)) (SNo_mul_SNo z0 w1 Hz0a Hw1a)) (SNo_add_SNo (x * w1) (z0 * w1') (SNo_mul_SNo x w1 Hx1 Hw1a) (SNo_mul_SNo z0 w1' Hz0a (HLRy1 w1' Hw1'1))) to the current goal.
We will prove x * w1' + z0 * w1 ≤ x * w1 + z0 * w1'.
rewrite the current goal using add_SNo_com (x * w1) (z0 * w1') (SNo_mul_SNo x w1 Hx1 Hw1a) (SNo_mul_SNo z0 w1' Hz0a (HLRy1 w1' Hw1'1)) (from left to right).
Apply mul_SNo_Le z0 w1' x w1 Hz0a (HLRy1 w1' Hw1'1) Hx1 Hw1a to the current goal.
We will prove x ≤ z0.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hz0c.
We will prove w1 ≤ w1'.
An exact proof term for the current goal is Hw1'2.
We will prove z0' * y + x * w1 + z0 * w1' ≤ z0 * y + x * w1 + z0' * w1'.
rewrite the current goal using add_SNo_com_3_0_1 (z0' * y) (x * w1) (z0 * w1') (SNo_mul_SNo z0' y (HLRx2 z0' Hz0'1) Hy1) (SNo_mul_SNo x w1 Hx1 Hw1a) (SNo_mul_SNo z0 w1' Hz0a (HLRy1 w1' Hw1'1)) (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (z0 * y) (x * w1) (z0' * w1') (SNo_mul_SNo z0 y Hz0a Hy1) (SNo_mul_SNo x w1 Hx1 Hw1a) (SNo_mul_SNo z0' w1' (HLRx2 z0' Hz0'1) (HLRy1 w1' Hw1'1)) (from left to right).
We will prove x * w1 + z0' * y + z0 * w1' ≤ x * w1 + z0 * y + z0' * w1'.
Apply add_SNo_Le2 (x * w1) (z0' * y + z0 * w1') (z0 * y + z0' * w1') (SNo_mul_SNo x w1 Hx1 Hw1a) (SNo_add_SNo (z0' * y) (z0 * w1') (SNo_mul_SNo z0' y (HLRx2 z0' Hz0'1) Hy1) (SNo_mul_SNo z0 w1' Hz0a (HLRy1 w1' Hw1'1))) (SNo_add_SNo (z0 * y) (z0' * w1') (SNo_mul_SNo z0 y Hz0a Hy1) (SNo_mul_SNo z0' w1' (HLRx2 z0' Hz0'1) (HLRy1 w1' Hw1'1))) to the current goal.
We will prove z0' * y + z0 * w1' ≤ z0 * y + z0' * w1'.
Apply mul_SNo_Le z0 y z0' w1' Hz0a Hy1 (HLRx2 z0' Hz0'1) (HLRy1 w1' Hw1'1) to the current goal.
We will prove z0' ≤ z0.
An exact proof term for the current goal is Hz0'2.
We will prove w1' ≤ y.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hy3 w1' Hw1'1.
rewrite the current goal using HLR'eq (from right to left).
We will prove ∀w ∈ LxLy' ∪ RxRy', w < x * y.
Let w be given.
Apply binunionE' to the current goal.
Assume Hw: w ∈ LxLy'.
Apply LxLy'E w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ Lx.
Let w'' be given.
Assume Hw'': w'' ∈ Ly.
Assume Hw'1: SNo w'.
Assume Hw''1: SNo w''.
Assume Hw'2: w' < x.
Assume Hw''2: w'' < y.
Assume Hwe.
rewrite the current goal using Hwe (from left to right).
We will prove w' * y + x * w'' + - w' * w'' < x * y.
Apply add_SNo_minus_Lt1b3 (w' * y) (x * w'') (w' * w'') (x * y) (SNo_mul_SNo w' y Hw'1 Hy1) (SNo_mul_SNo x w'' Hx1 Hw''1) (SNo_mul_SNo w' w'' Hw'1 Hw''1) (SNo_mul_SNo x y Hx1 Hy1) to the current goal.
We will prove w' * y + x * w'' < x * y + w' * w''.
An exact proof term for the current goal is mul_SNo_Lt x y w' w'' Hx1 Hy1 Hw'1 Hw''1 Hw'2 Hw''2.
Assume Hw: w ∈ RxRy'.
Apply RxRy'E w Hw to the current goal.
Let z be given.
Assume Hz: z ∈ Rx.
Let z' be given.
Assume Hz': z' ∈ Ry.
Assume Hz1: SNo z.
Assume Hz'1: SNo z'.
Assume Hz2: x < z.
Assume Hz'2: y < z'.
Assume Hwe.
rewrite the current goal using Hwe (from left to right).
We will prove z * y + x * z' + - z * z' < x * y.
Apply add_SNo_minus_Lt1b3 (z * y) (x * z') (z * z') (x * y) (SNo_mul_SNo z y Hz1 Hy1) (SNo_mul_SNo x z' Hx1 Hz'1) (SNo_mul_SNo z z' Hz1 Hz'1) (SNo_mul_SNo x y Hx1 Hy1) to the current goal.
We will prove z * y + x * z' < x * y + z * z'.
rewrite the current goal using add_SNo_com (z * y) (x * z') (SNo_mul_SNo z y Hz1 Hy1) (SNo_mul_SNo x z' Hx1 Hz'1) (from left to right).
rewrite the current goal using add_SNo_com (x * y) (z * z') (SNo_mul_SNo x y Hx1 Hy1) (SNo_mul_SNo z z' Hz1 Hz'1) (from left to right).
An exact proof term for the current goal is mul_SNo_Lt z z' x y Hz1 Hz'1 Hx1 Hy1 Hz2 Hz'2.
rewrite the current goal using HLR'eq (from right to left).
We will prove ∀z ∈ LxRy' ∪ RxLy', x * y < z.
Let z be given.
Apply binunionE' to the current goal.
Assume Hz: z ∈ LxRy'.
Apply LxRy'E z Hz to the current goal.
Let w be given.
Assume Hw: w ∈ Lx.
Let z' be given.
Assume Hz': z' ∈ Ry.
Assume Hw1: SNo w.
Assume Hz'1: SNo z'.
Assume Hw2: w < x.
Assume Hz'2: y < z'.
Assume Hze.
rewrite the current goal using Hze (from left to right).
We will prove x * y < w * y + x * z' + - w * z'.
Apply add_SNo_minus_Lt2b3 (w * y) (x * z') (w * z') (x * y) (SNo_mul_SNo w y Hw1 Hy1) (SNo_mul_SNo x z' Hx1 Hz'1) (SNo_mul_SNo w z' Hw1 Hz'1) (SNo_mul_SNo x y Hx1 Hy1) to the current goal.
We will prove x * y + w * z' < w * y + x * z'.
rewrite the current goal using add_SNo_com (x * y) (w * z') (SNo_mul_SNo x y Hx1 Hy1) (SNo_mul_SNo w z' Hw1 Hz'1) (from left to right).
rewrite the current goal using add_SNo_com (w * y) (x * z') (SNo_mul_SNo w y Hw1 Hy1) (SNo_mul_SNo x z' Hx1 Hz'1) (from left to right).
We will prove w * z' + x * y < x * z' + w * y.
An exact proof term for the current goal is mul_SNo_Lt x z' w y Hx1 Hz'1 Hw1 Hy1 Hw2 Hz'2.
Assume Hz: z ∈ RxLy'.
Apply RxLy'E z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Rx.
Let w be given.
Assume Hw: w ∈ Ly.
Assume Hz'1: SNo z'.
Assume Hw1: SNo w.
Assume Hz'2: x < z'.
Assume Hw2: w < y.
Assume Hze.
rewrite the current goal using Hze (from left to right).
We will prove x * y < z' * y + x * w + - z' * w.
Apply add_SNo_minus_Lt2b3 (z' * y) (x * w) (z' * w) (x * y) (SNo_mul_SNo z' y Hz'1 Hy1) (SNo_mul_SNo x w Hx1 Hw1) (SNo_mul_SNo z' w Hz'1 Hw1) (SNo_mul_SNo x y Hx1 Hy1) to the current goal.
We will prove x * y + z' * w < z' * y + x * w.
An exact proof term for the current goal is mul_SNo_Lt z' y x w Hz'1 Hy1 Hx1 Hw1 Hz'2 Hw2.
Apply and3I to the current goal.
An exact proof term for the current goal is L1.
An exact proof term for the current goal is Lxyeq.
Let q be given.
Assume Hq.
Apply Hq LxLy' RxRy' LxRy' RxLy' to the current goal.
An exact proof term for the current goal is LxLy'E.
An exact proof term for the current goal is LxLy'I.
An exact proof term for the current goal is RxRy'E.
An exact proof term for the current goal is RxRy'I.
An exact proof term for the current goal is LxRy'E.
An exact proof term for the current goal is LxRy'I.
An exact proof term for the current goal is RxLy'E.
An exact proof term for the current goal is RxLy'I.
An exact proof term for the current goal is L1.
An exact proof term for the current goal is Lxyeq.
∎