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