Let x, y, z, w and u be given.
Assume Hx Hy Hz Hw Hu.
rewrite the current goal using add_SNo_com (x + y + z) (w + u) (SNo_add_SNo_3 x y z Hx Hy Hz) (SNo_add_SNo w u Hw Hu) (from left to right).
We will prove (w + u) + (x + y + z) = (u + y + z) + (w + x).
rewrite the current goal using add_SNo_com_4_inner_mid w u x (y + z) Hw Hu Hx (SNo_add_SNo y z Hy Hz) (from left to right).
We will prove (w + x) + (u + y + z) = (u + y + z) + (w + x).
An exact proof term for the current goal is add_SNo_com (w + x) (u + y + z) (SNo_add_SNo w x Hw Hx) (SNo_add_SNo_3 u y z Hu Hy Hz).
∎