Let z be given.
Assume Hz2a Hz2b.
We prove the intermediate
claim Lzy:
z ∈ SNoL y.
An
exact proof term for the current goal is
SNoL_I y Hy z Hz1 Hz2b Hz6.
We prove the intermediate
claim Lzv:
z ∈ SNoR v.
An
exact proof term for the current goal is
SNoR_I v Hv z Hz1 Hz2a Hz5.
We prove the intermediate
claim Lxz:
SNo (x * z).
An
exact proof term for the current goal is
SNo_mul_SNo x z Hx Hz1.
We prove the intermediate
claim Luz:
SNo (u * z).
An
exact proof term for the current goal is
SNo_mul_SNo u z Hu Hz1.
We prove the intermediate
claim Lwz:
SNo (w * z).
An
exact proof term for the current goal is
SNo_mul_SNo w z Hw1 Hz1.
We prove the intermediate
claim L1:
w * y + x * z < x * y + w * z.
An exact proof term for the current goal is Hxy1 w Lwx z Lzy.
We prove the intermediate
claim L2:
w * v + u * z < u * v + w * z.
An exact proof term for the current goal is Huv2 w Lwu z Lzv.
We prove the intermediate
claim L3:
x * v + w * z < w * v + x * z.
An exact proof term for the current goal is Hxv3 w Lwx z Lzv.
We prove the intermediate
claim L4:
u * y + w * z < w * y + u * z.
An exact proof term for the current goal is Huy4 w Lwu z Lzy.
We prove the intermediate
claim Lwzwz:
SNo (w * z + w * z).
An
exact proof term for the current goal is
SNo_add_SNo (w * z) (w * z) Lwz Lwz.
We will
prove (u * y + x * v) + (w * z + w * z) < (x * y + u * v) + (w * z + w * z).
We prove the intermediate
claim Lwyuz:
SNo (w * y + u * z).
An
exact proof term for the current goal is
SNo_add_SNo (w * y) (u * z) Lwy Luz.
We prove the intermediate
claim Lwvxz:
SNo (w * v + x * z).
An
exact proof term for the current goal is
SNo_add_SNo (w * v) (x * z) Lwv Lxz.
We prove the intermediate
claim Luywz:
SNo (u * y + w * z).
An
exact proof term for the current goal is
SNo_add_SNo (u * y) (w * z) Huy Lwz.
We prove the intermediate
claim Lxvwz:
SNo (x * v + w * z).
An
exact proof term for the current goal is
SNo_add_SNo (x * v) (w * z) Hxv Lwz.
We prove the intermediate
claim Lwvuz:
SNo (w * v + u * z).
An
exact proof term for the current goal is
SNo_add_SNo (w * v) (u * z) Lwv Luz.
We prove the intermediate
claim Lxyxz:
SNo (x * y + x * z).
An
exact proof term for the current goal is
SNo_add_SNo (x * y) (x * z) Hxy Lxz.
We prove the intermediate
claim Lwyxz:
SNo (w * y + x * z).
An
exact proof term for the current goal is
SNo_add_SNo (w * y) (x * z) Lwy Lxz.
We prove the intermediate
claim Lxywz:
SNo (x * y + w * z).
An
exact proof term for the current goal is
SNo_add_SNo (x * y) (w * z) Hxy Lwz.
We prove the intermediate
claim Luvwz:
SNo (u * v + w * z).
An
exact proof term for the current goal is
SNo_add_SNo (u * v) (w * z) Huv Lwz.
We will
prove (u * y + x * v) + (w * z + w * z) < (w * y + u * z) + (w * v + x * z).
We will
prove (u * y + w * z) + (x * v + w * z) < (w * y + u * z) + (w * v + x * z).
Apply add_SNo_Lt3 (u * y + w * z) (x * v + w * z) (w * y + u * z) (w * v + x * z) Luywz Lxvwz Lwyuz Lwvxz to the current goal.
We will
prove u * y + w * z < w * y + u * z.
An exact proof term for the current goal is L4.
We will
prove x * v + w * z < w * v + x * z.
An exact proof term for the current goal is L3.
We will
prove (w * y + u * z) + (w * v + x * z) < (x * y + u * v) + (w * z + w * z).
We will
prove (w * y + u * z) + (w * v + x * z) < (x * y + w * z) + (u * v + w * z).
rewrite the current goal using
add_SNo_com (w * y) (u * z) Lwy Luz (from left to right).
rewrite the current goal using
add_SNo_com (w * v) (u * z) Lwv Luz (from right to left).
We will
prove (w * v + u * z) + (w * y + x * z) < (x * y + w * z) + (u * v + w * z).
rewrite the current goal using
add_SNo_com (w * v + u * z) (w * y + x * z) Lwvuz Lwyxz (from left to right).
We will
prove (w * y + x * z) + (w * v + u * z) < (x * y + w * z) + (u * v + w * z).
Apply add_SNo_Lt3 (w * y + x * z) (w * v + u * z) (x * y + w * z) (u * v + w * z) Lwyxz Lwvuz Lxywz Luvwz to the current goal.
An exact proof term for the current goal is L1.
An exact proof term for the current goal is L2.