Let x, y and z be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hz: SNo z.
Assume Hxyz: x + y = z + y.
We prove the intermediate claim L1: y + x = y + z.
rewrite the current goal using add_SNo_com y x Hy Hx (from left to right).
rewrite the current goal using add_SNo_com y z Hy Hz (from left to right).
An exact proof term for the current goal is Hxyz.
An exact proof term for the current goal is add_SNo_cancel_L y x z Hy Hx Hz L1.
∎