Let x, y, z and w be given.
Assume Hx Hy Hz Hw Hxnn Hynn Hxz Hyw.
Apply SNoLe_tra (x * y) (x * w) (z * w) (SNo_mul_SNo x y Hx Hy) (SNo_mul_SNo x w Hx Hw) (SNo_mul_SNo z w Hz Hw) to the current goal.
We will prove x * y ≤ x * w.
An exact proof term for the current goal is nonneg_mul_SNo_Le x y w Hx Hxnn Hy Hw Hyw.
We will prove x * w ≤ z * w.
Apply nonneg_mul_SNo_Le' x z w Hx Hz Hw to the current goal.
We will prove 0 ≤ w.
An exact proof term for the current goal is SNoLe_tra 0 y w SNo_0 Hy Hw Hynn Hyw.
An exact proof term for the current goal is Hxz.
∎