Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
Use transitivity with (x + y) + z + w, and ((x + y) + z) + w.
An exact proof term for the current goal is add_SNo_assoc x y (z + w) Hx Hy (SNo_add_SNo z w Hz Hw).
An exact proof term for the current goal is add_SNo_assoc (x + y) z w (SNo_add_SNo x y Hx Hy) Hz Hw.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is add_SNo_assoc x y z Hx Hy Hz.
∎