Let x, y, z, w, u and v be given.
Assume Hx Hy Hz Hw Hu Hv H1 H2.
Apply add_SNo_Lt1_cancel (x + y) (u + v) (z + w) (SNo_add_SNo x y Hx Hy) (SNo_add_SNo u v Hu Hv) (SNo_add_SNo z w Hz Hw) to the current goal.
We will prove (x + y) + (u + v) < (z + w) + (u + v).
rewrite the current goal using add_SNo_com_4_inner_mid x y u v Hx Hy Hu Hv (from left to right).
We will prove (x + u) + (y + v) < (z + w) + (u + v).
We prove the intermediate claim L1: (z + w) + (u + v) = (z + v) + (w + u).
rewrite the current goal using add_SNo_assoc z w (u + v) Hz Hw (SNo_add_SNo u v Hu Hv) (from right to left).
rewrite the current goal using add_SNo_assoc z v (w + u) Hz Hv (SNo_add_SNo w u Hw Hu) (from right to left).
We will prove z + (w + (u + v)) = z + (v + (w + u)).
Use f_equal.
We will prove w + u + v = v + w + u.
An exact proof term for the current goal is add_SNo_rotate_3_1 w u v Hw Hu Hv.
rewrite the current goal using L1 (from left to right).
We will prove (x + u) + (y + v) < (z + v) + (w + u).
An exact proof term for the current goal is add_SNo_Lt3 (x + u) (y + v) (z + v) (w + u) (SNo_add_SNo x u Hx Hu) (SNo_add_SNo y v Hy Hv) (SNo_add_SNo z v Hz Hv) (SNo_add_SNo w u Hw Hu) H1 H2.
∎