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.
Assume Hux: u < x.
Apply SNoLeE v y Hv Hy Hvy to the current goal.
Assume Hvy: v < y.
Apply SNoLtLe 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.
Assume Hvy: v = y.
rewrite the current goal using Hvy (from left to right).
We will
prove u * y + x * y ≤ x * y + u * y.
rewrite the current goal using
add_SNo_com (u * y) (x * y) (SNo_mul_SNo u y Hu Hy) (SNo_mul_SNo x y Hx Hy) (from left to right).
We will
prove x * y + u * y ≤ x * y + u * y.
Apply SNoLe_ref to the current goal.
Assume Hux: u = x.
rewrite the current goal using Hux (from left to right).
We will
prove x * y + x * v ≤ x * y + x * v.
Apply SNoLe_ref to the current goal.