Let x, y and z be given.

Assume Hx Hy Hz Hzpos Hxy.

rewrite the current goal using mul_SNo_com x z Hx Hz (from left to right).

rewrite the current goal using mul_SNo_com y z Hy Hz (from left to right).

An exact proof term for the current goal is pos_mul_SNo_Lt z x y Hz Hzpos Hx Hy Hxy.

∎