Let u' be given.
Assume Hu'.
Let v' be given.
Assume Hv' Hze.
Apply SNoL_E x Hx u' Hu' to the current goal.
Assume _ _.
Apply SNoR_E y Hy v' Hv' to the current goal.
Assume _ _.
We prove the intermediate
claim Lu'y:
SNo (u' * y).
An
exact proof term for the current goal is
SNo_mul_SNo u' y Hu'a Hy.
We prove the intermediate
claim Lxv':
SNo (x * v').
An
exact proof term for the current goal is
SNo_mul_SNo x v' Hx Hv'a.
We prove the intermediate
claim Lu'v':
SNo (u' * v').
An
exact proof term for the current goal is
SNo_mul_SNo u' v' Hu'a Hv'a.
rewrite the current goal using Hwe (from left to right).
rewrite the current goal using Hze (from left to right).
We will
prove u * y + x * v + - u * v < u' * y + x * v' + - u' * v'.
We will
prove u * y + x * v + u' * v' < u' * y + x * v' + u * v.
We will
prove u * y + x * v + u' * v' < x * y + u * v + u' * v'.
We will
prove u * y + x * v < x * y + u * v.
An exact proof term for the current goal is Hxy1 u Hu v Hv.
We will
prove x * y + u * v + u' * v' < u' * y + x * v' + u * v.
Apply add_SNo_3_2_3_Lt1 (x * y) (u' * v') (u' * y) (x * v') (u * v) Hxy Lu'v' Lu'y Lxv' Luv to the current goal.
We will
prove u' * v' + x * y < u' * y + x * v'.
rewrite the current goal using
add_SNo_com (u' * v') (x * y) Lu'v' Hxy (from left to right).
An exact proof term for the current goal is Hxy3 u' Hu' v' Hv'.