Let x, y, w, u, v and a be given.
Assume Hx Hy Hw Hu Hv Ha H1 H2.
rewrite the current goal using
add_SNo_com x y Hx Hy (from left to right).
We will
prove y + x < w + u + v.
We will
prove y + x < u + v + w.
rewrite the current goal using
add_SNo_0R x Hx (from right to left).
We will
prove y + x + 0 < u + v + w.
We will
prove y + 0 < u + a.
rewrite the current goal using
add_SNo_0R y Hy (from left to right).
rewrite the current goal using
add_SNo_com u a Hu Ha (from left to right).
An exact proof term for the current goal is H2.
We will
prove x + a < v + w.
rewrite the current goal using
add_SNo_com v w Hv Hw (from left to right).
An exact proof term for the current goal is H1.
∎