Let x, y, z, w, u and a be given.
Assume Hx Hy Hz Hw Hu Ha H1 H2.
Apply SNoLt_tra (x + y + z) (y + w + a) (w + u) (SNo_add_SNo x (y + z) Hx (SNo_add_SNo y z Hy Hz)) (SNo_add_SNo y (w + a) Hy (SNo_add_SNo w a Hw Ha)) (SNo_add_SNo w u Hw Hu) to the current goal.
We will prove x + y + z < y + w + a.
rewrite the current goal using add_SNo_com_3_0_1 x y z Hx Hy Hz (from left to right).
We will prove y + x + z < y + w + a.
Apply add_SNo_Lt2 y (x + z) (w + a) Hy (SNo_add_SNo x z Hx Hz) (SNo_add_SNo w a Hw Ha) to the current goal.
An exact proof term for the current goal is H1.
We will prove y + w + a < w + u.
rewrite the current goal using add_SNo_rotate_3_1 w a y Hw Ha Hy (from right to left).
We will prove w + a + y < w + u.
Apply add_SNo_Lt2 w (a + y) u Hw (SNo_add_SNo a y Ha Hy) Hu to the current goal.
We will prove a + y < u.
rewrite the current goal using add_SNo_com a y Ha Hy (from left to right).
An exact proof term for the current goal is H2.
∎