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

Assume Hx Hy Hz Hw Hu Hv Hxw Hyu Hzv.

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

Apply add_SNo_Lt3 x (y + z) w (u + v) Hx (SNo_add_SNo y z Hy Hz) Hw (SNo_add_SNo u v Hu Hv) Hxw to the current goal.

We will prove y + z < u + v.

An exact proof term for the current goal is add_SNo_Lt3 y z u v Hy Hz Hu Hv Hyu Hzv.

∎