Let x, y and z be given.
Assume Hx1 Hx2 Hy Hz Hzy.
We will
prove x * y < x * z.
We prove the intermediate
claim L1:
x * y + 0 * z = x * y.
Use transitivity with and
x * y + 0.
An
exact proof term for the current goal is
add_SNo_0R (x * y) (SNo_mul_SNo x y Hx1 Hy).
We prove the intermediate
claim L2:
0 * y + x * z = x * z.
Use transitivity with and
0 + x * z.
An
exact proof term for the current goal is
add_SNo_0L (x * z) (SNo_mul_SNo x z Hx1 Hz).
rewrite the current goal using L1 (from right to left).
rewrite the current goal using L2 (from right to left).
An
exact proof term for the current goal is
mul_SNo_Lt 0 y x z SNo_0 Hy Hx1 Hz Hx2 Hzy.