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.
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_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.
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_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_Lt x z 0 y Hx1 Hz SNo_0 Hy Hx2 Hyz.
∎