Let x, y and z be given.
Assume Hx1 Hx2 Hy Hz Hyz.
We will
prove x * y ≤ x * z.
We prove the intermediate
claim L1:
0 * z + x * y = x * y.
Use transitivity with and
0 + x * y.
An
exact proof term for the current goal is
add_SNo_0L (x * y) (SNo_mul_SNo x y Hx1 Hy).
We prove the intermediate
claim L2:
x * z + 0 * y = x * z.
Use transitivity with and
x * z + 0.
An
exact proof term for the current goal is
add_SNo_0R (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_Le x z 0 y Hx1 Hz SNo_0 Hy Hx2 Hyz.