Let x, y and z be given.
Assume Hx Hy Hz.
We will
prove (x + y) + z = (x + z) + y.
rewrite the current goal using add_HSNo_assoc x y z Hx Hy Hz (from left to right).
We will
prove x + y + z = (x + z) + y.
rewrite the current goal using add_HSNo_assoc x z y Hx Hz Hy (from left to right).
We will
prove x + y + z = x + z + y.
Use f_equal.
An exact proof term for the current goal is add_HSNo_com y z Hy Hz.
∎