Let x, y, z, w and u be given.

Assume Hx Hy Hz Hw Hu H1.

rewrite the current goal using add_SNo_rotate_3_1 x u y Hx Hu Hy (from left to right).

We will prove y + x + u < z + w + u.

An exact proof term for the current goal is add_SNo_3_3_3_Lt1 y x z w u Hy Hx Hz Hw Hu H1.

∎