Let x, y and z be given.

Assume Hx Hy Hz.

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

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

Use f_equal.

An exact proof term for the current goal is add_SNo_com y z Hy Hz.

∎