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.
rewrite the current goal using add_SNo_rotate_3_1 u v w Hu Hv Hw (from right to left).
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.
Apply add_SNo_Lt_subprop3a y x 0 u (v + w) a Hy Hx SNo_0 Hu (SNo_add_SNo v w Hv Hw) Ha to the current goal.
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.