Let x, y, u and v be given.
Assume Hx Hy Hu Hv Hux Hvy.
Apply SNoLeE u x Hu Hx Hux to the current goal.
Apply SNoLeE v y Hv Hy Hvy to the current goal.
An
exact proof term for the current goal is
mul_SNo_Lt x y u v Hx Hy Hu Hv Hux Hvy.
rewrite the current goal using Hvy (from left to right).
We will
prove u * y + x * y ≤ x * y + u * y.
We will
prove x * y + u * y ≤ x * y + u * y.
rewrite the current goal using Hux (from left to right).
We will
prove x * y + x * v ≤ x * y + x * v.
∎