Let x and y be given.

Assume Hx Hy.

rewrite the current goal using add_SNo_com (- x) (x + y) (SNo_minus_SNo x Hx) (SNo_add_SNo x y Hx Hy) (from left to right).

We will prove (x + y) + - x = y.

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

We will prove (y + x) + - x = y.

An exact proof term for the current goal is add_SNo_minus_R2 y x Hy Hx.

∎