Let x and y be given.

Assume Hx Hy.

Use transitivity with x + (y + - y), and x + 0.

Use symmetry.

An exact proof term for the current goal is add_SNo_assoc x y (- y) Hx Hy (SNo_minus_SNo y Hy).

Use f_equal.

An exact proof term for the current goal is add_SNo_minus_SNo_rinv y Hy.

An exact proof term for the current goal is add_SNo_0R x Hx.

∎