Let x, y, z and w be given.

Assume Hx Hy Hz Hw.

rewrite the current goal using add_HSNo_assoc (x + y) z w (HSNo_add_HSNo x y Hx Hy) Hz Hw (from right to left).

We will prove ((x + y) + z) + w = (x + z) + (y + w).

rewrite the current goal using add_HSNo_com_3b_1_2 x y z Hx Hy Hz (from left to right).

We will prove ((x + z) + y) + w = (x + z) + (y + w).

An exact proof term for the current goal is add_HSNo_assoc (x + z) y w (HSNo_add_HSNo x z Hx Hz) Hy Hw.

∎