Let x, y and z be given.

Assume Hx: SNo x.

Assume Hy: SNo y.

Assume Hz: SNo z.

Assume Hxyz: x + y = x + z.

We prove the intermediate claim Lmx: SNo (- x).

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

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

rewrite the current goal using Hxyz (from left to right).

An exact proof term for the current goal is add_SNo_minus_L2 x z Hx Hz.

∎