Let x, y, z and w be given.

Assume Hx Hy Hz Hw.

rewrite the current goal using add_CSNo_assoc (x + y) z w (CSNo_add_CSNo 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_CSNo_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_CSNo_assoc (x + z) y w (CSNo_add_CSNo x z Hx Hz) Hy Hw.

∎