Let x, y and z be given.

Assume Hx Hy Hz Hznn 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 nonneg_mul_SNo_Le z x y Hz Hznn Hx Hy Hxy.

∎