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_CSNo_com y z Hy Hz.
Use symmetry.
An exact proof term for the current goal is add_CSNo_assoc x z y Hx Hz Hy.
Use f_equal.
An exact proof term for the current goal is add_CSNo_com x z Hx Hz.
An exact proof term for the current goal is add_CSNo_assoc z x y Hz Hx Hy.