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.
Use f_equal.
We will prove 0 * z = 0.
An exact proof term for the current goal is mul_SNo_zeroL z Hz.
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.
Use f_equal.
An exact proof term for the current goal is mul_SNo_zeroL y Hy.
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.
∎