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.
Apply HLRy to the current goal.
Assume H .
Apply H to the current goal.
rewrite the current goal using Hxe (from right to left).
rewrite the current goal using Hye (from right to left).
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 .
Let ww' be given.
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 .
An
exact proof term for the current goal is
Hx3 (ww' 0 ) Lww'0 .
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 .
Let zz' be given.
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 .
An
exact proof term for the current goal is
Hx4 (zz' 0 ) Lzz'0 .
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 .
Let wz be given.
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 .
An
exact proof term for the current goal is
Hx3 (wz 0 ) Lwz0 .
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 .
Let zw be given.
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 .
An
exact proof term for the current goal is
Hx4 (zw 0 ) Lzw0 .
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' ) .
Apply and3I to the current goal.
Let w be given.
Apply LxLy'E w Hw to the current goal.
Let w' be given.
Let w'' be given.
Assume Hwe .
rewrite the current goal using Hwe (from left to right).
We will
prove SNo (w' * y + x * w'' + - w' * w'' ) .
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 .
An
exact proof term for the current goal is
SNo_mul_SNo w' w'' Hw'1 Hw''1 .
Apply RxRy'E w Hw to the current goal.
Let z' be given.
Let z'' be given.
Assume Hwe .
rewrite the current goal using Hwe (from left to right).
We will
prove SNo (z' * y + x * z'' + - z' * z'' ) .
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 .
An
exact proof term for the current goal is
SNo_mul_SNo z' z'' Hz'1 Hz''1 .
Let z be given.
Apply LxRy'E z Hz to the current goal.
Let w' be given.
Let z' be given.
Assume Hze .
rewrite the current goal using Hze (from left to right).
We will
prove SNo (w' * y + x * z' + - w' * z' ) .
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 .
An
exact proof term for the current goal is
SNo_mul_SNo w' z' Hw'1 Hz'1 .
Apply RxLy'E z Hz to the current goal.
Let z' be given.
Let w' be given.
Assume Hze .
rewrite the current goal using Hze (from left to right).
We will
prove SNo (z' * y + x * w' + - z' * w' ) .
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 .
An
exact proof term for the current goal is
SNo_mul_SNo z' w' Hz'1 Hw'1 .
Let w be given.
Apply LxLy'E w Hw to the current goal.
Let w' be given.
Let w'' be given.
Assume Hwe .
rewrite the current goal using Hwe (from left to right).
Let z be given.
Apply LxRy'E z Hz to the current goal.
Let w''' be given.
Let z' be given.
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' .
We will
prove w' * y + x * w'' + w''' * z' < w''' * y + x * z' + w' * w'' .
We will
prove w' * y + x * w'' + w''' * z' < x * y + w' * w'' + w''' * z' .
We will
prove w''' * z' + w' * y + x * w'' < w''' * z' + x * y + w' * w'' .
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'' .
We will
prove w' * w'' + x * y + w''' * z' < w' * w'' + w''' * y + x * z' .
We will
prove x * y + w''' * z' < w''' * y + x * z' .
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 .
Apply RxLy'E z Hz to the current goal.
Let z' be given.
Let w''' be given.
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''' .
We will
prove w' * y + x * w'' + z' * w''' < z' * y + x * w''' + w' * w'' .
We will
prove w' * y + x * w'' + z' * w''' < z' * w''' + x * y + w' * w'' .
We will
prove z' * w''' + w' * y + x * w'' < z' * w''' + x * y + w' * w'' .
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'' .
We will
prove w' * w'' + z' * w''' + x * y < w' * w'' + z' * y + x * w''' .
We will
prove z' * w''' + x * y < z' * y + x * w''' .
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 .
Apply RxRy'E w Hw to the current goal.
Let z' be given.
Let z'' be given.
Assume Hwe .
rewrite the current goal using Hwe (from left to right).
Let z be given.
Apply LxRy'E z Hz to the current goal.
Let w' be given.
Let z''' be given.
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''' .
We will
prove z' * y + x * z'' + w' * z''' < w' * y + x * z''' + z' * z'' .
We will
prove z' * y + x * z'' + w' * z''' < w' * z''' + z' * z'' + x * y .
We will
prove w' * z''' + z' * y + x * z'' < w' * z''' + z' * z'' + x * y .
We will
prove z' * y + x * z'' < 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 w' * z''' + z' * z'' + x * y < w' * y + x * z''' + z' * z'' .
We will
prove z' * z'' + w' * z''' + x * y < z' * z'' + w' * y + x * z''' .
We will
prove w' * z''' + x * y < w' * y + x * z''' .
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 .
Apply RxLy'E z Hz to the current goal.
Let z''' be given.
Let w' be given.
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' .
We will
prove z' * y + x * z'' + z''' * w' < z''' * y + x * w' + z' * z'' .
We will
prove z' * y + x * z'' + z''' * w' < z''' * w' + z' * z'' + x * y .
We will
prove z''' * w' + x * z'' + z' * y < z''' * w' + z' * z'' + x * y .
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'' .
We will
prove z' * z'' + z''' * w' + x * y < z' * z'' + z''' * y + x * w' .
We will
prove z''' * w' + x * y < 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 .
We prove the intermediate
claim Lxyeq :
x * y = SNoCut (LxLy' ∪ RxRy' ) (LxRy' ∪ RxLy' ) .
Set v to be the term
SNoCut (LxLy' ∪ RxRy' ) (LxRy' ∪ RxLy' ) .
Let L' and R' be given.
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.
Let w1 be given.
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 .
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 .
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' .
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.
An exact proof term for the current goal is Hw0c .
An exact proof term for the current goal is Hx4 z' Hz' .
Apply L2a to the current goal.
Assume _ .
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 .
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 .
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' .
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.
An exact proof term for the current goal is Hw1c .
An exact proof term for the current goal is Hy4 z' Hz' .
Apply L3a to the current goal.
Assume _ .
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.
Apply L3 to the current goal.
Let w1' be given.
Assume H .
Apply H to the current goal.
We will
prove w0 * y + x * w1 + - w0 * w1 < v .
We will
prove w0 * y + x * w1 + - w0 * w1 ≤ w0' * y + x * w1' + - w0' * w1' .
We will
prove w0 * y + x * w1 + w0' * w1' ≤ w0' * y + x * w1' + w0 * w1 .
We will
prove w0 * y + x * w1 + w0' * w1' ≤ w0 * y + x * w1' + w0' * w1 .
We will
prove x * w1 + w0' * w1' ≤ x * w1' + w0' * w1 .
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.
An exact proof term for the current goal is Hx3 w0' Hw0'1 .
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 .
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.
An exact proof term for the current goal is Hw0'2 .
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 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.
Let z1 be given.
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 .
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.
An exact proof term for the current goal is Hx3 w' Hw' .
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 .
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' .
An exact proof term for the current goal is H .
Apply L4a to the current goal.
Assume _ .
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 .
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.
An exact proof term for the current goal is Hy3 w' Hw' .
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 .
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' .
An exact proof term for the current goal is H .
Apply L5a to the current goal.
Assume _ .
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.
Apply L5 to the current goal.
Let z1' be given.
Assume H .
Apply H to the current goal.
We will
prove z0 * y + x * z1 + - z0 * z1 < v .
We will
prove z0 * y + x * z1 + - z0 * z1 ≤ z0' * y + x * z1' + - z0' * z1' .
We will
prove z0 * y + x * z1 + z0' * z1' ≤ z0' * y + x * z1' + z0 * z1 .
We will
prove z0 * y + x * z1 + z0' * z1' ≤ z0 * y + z0' * z1 + x * z1' .
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.
An exact proof term for the current goal is Hx4 z0' Hz0'1 .
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 .
We will
prove x * z1' + z0 * y + z0' * z1 ≤ x * z1' + z0' * y + z0 * z1 .
We will
prove z0 * y + z0' * z1 ≤ z0' * y + z0 * z1 .
Apply mul_SNo_Le z0 z1 z0' y Hz0a Hz1a (HLRx2 z0' Hz0'1 ) Hy1 to the current goal.
An exact proof term for the current goal is Hz0'2 .
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 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.
Let z1 be given.
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 .
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 .
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' .
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.
An exact proof term for the current goal is Hw0c .
An exact proof term for the current goal is Hx4 z' Hz' .
Apply L6a to the current goal.
Assume _ .
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 .
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.
An exact proof term for the current goal is Hy3 w' Hw' .
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 .
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' .
An exact proof term for the current goal is H .
Apply L7a to the current goal.
Assume _ .
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.
Apply L7 to the current goal.
Let z1' be given.
Assume H .
Apply H to the current goal.
We will
prove v < w0 * y + x * z1 + - w0 * z1 .
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 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 .
We will
prove w0' * y + x * z1' + w0 * z1 ≤ w0 * y + x * z1 + w0' * z1' .
We will
prove w0' * y + x * z1' + w0 * z1 ≤ x * z1' + w0' * z1 + w0 * y .
We will
prove w0' * y + w0 * z1 ≤ w0' * z1 + w0 * y .
Apply mul_SNo_Le w0' z1 w0 y (HLRx1 w0' Hw0'1 ) Hz1a Hw0a Hy1 to the current goal.
An exact proof term for the current goal is Hw0'2 .
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' .
We will
prove w0 * y + x * z1' + w0' * z1 ≤ w0 * y + x * z1 + w0' * z1' .
We will
prove x * z1' + w0' * z1 ≤ x * z1 + w0' * z1' .
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.
An exact proof term for the current goal is Hx3 w0' Hw0'1 .
An exact proof term for the current goal is Hz1'2 .
Let z0 be given.
Let w1 be given.
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 .
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.
An exact proof term for the current goal is Hx3 w' Hw' .
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 .
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' .
An exact proof term for the current goal is H .
Apply L8a to the current goal.
Assume _ .
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 .
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 .
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' .
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.
An exact proof term for the current goal is Hw1c .
An exact proof term for the current goal is Hy4 z' Hz' .
Apply L9a to the current goal.
Assume _ .
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.
Apply L9 to the current goal.
Let w1' be given.
Assume H .
Apply H to the current goal.
We will
prove v < z0 * y + x * w1 + - z0 * w1 .
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 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 .
We will
prove z0' * y + x * w1' + z0 * w1 ≤ z0 * y + x * w1 + z0' * w1' .
We will
prove z0' * y + x * w1' + z0 * w1 ≤ z0' * y + x * w1 + z0 * w1' .
We will
prove x * w1' + z0 * w1 ≤ x * w1 + z0 * w1' .
Apply mul_SNo_Le z0 w1' x w1 Hz0a (HLRy1 w1' Hw1'1 ) Hx1 Hw1a to the current goal.
An exact proof term for the current goal is Hz0c .
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' .
We will
prove x * w1 + z0' * y + z0 * w1' ≤ x * w1 + z0 * y + z0' * w1' .
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.
An exact proof term for the current goal is Hz0'2 .
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 LxLy'E w Hw to the current goal.
Let w' be given.
Let w'' be given.
Assume Hwe .
rewrite the current goal using Hwe (from left to right).
We will
prove w' * y + x * w'' + - w' * w'' < x * y .
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 .
Apply RxRy'E w Hw to the current goal.
Let z be given.
Let z' be given.
Assume Hwe .
rewrite the current goal using Hwe (from left to right).
We will
prove z * y + x * z' + - z * z' < x * y .
We will
prove z * y + x * z' < x * y + z * z' .
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 LxRy'E z Hz to the current goal.
Let w be given.
Let z' be given.
Assume Hze .
rewrite the current goal using Hze (from left to right).
We will
prove x * y < w * y + x * z' + - w * z' .
We will
prove x * y + w * z' < w * y + x * z' .
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 .
Apply RxLy'E z Hz to the current goal.
Let z' be given.
Let w be given.
Assume Hze .
rewrite the current goal using Hze (from left to right).
We will
prove x * y < z' * y + x * w + - z' * w .
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 .
∎