Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
We prove the intermediate claim Lmy: SNo (- y).
An exact proof term for the current goal is SNo_minus_SNo y Hy.
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx Hy.
We prove the intermediate claim L1: (x + y) + - (x + y) = (x + y) + ((- x) + (- y)).
rewrite the current goal using add_SNo_minus_SNo_rinv (x + y) Lxy (from left to right).
We will prove 0 = (x + y) + ((- x) + (- y)).
rewrite the current goal using add_SNo_assoc (x + y) (- x) (- y) Lxy Lmx Lmy (from left to right).
We will prove 0 = ((x + y) + (- x)) + (- y).
rewrite the current goal using add_SNo_com x y Hx Hy (from left to right).
We will prove 0 = ((y + x) + - x) + - y.
rewrite the current goal using add_SNo_assoc y x (- x) Hy Hx Lmx (from right to left).
We will prove 0 = (y + (x + - x)) + - y.
rewrite the current goal using add_SNo_minus_SNo_rinv x Hx (from left to right).
We will prove 0 = (y + 0) + - y.
rewrite the current goal using add_SNo_0R y Hy (from left to right).
We will prove 0 = y + - y.
rewrite the current goal using add_SNo_minus_SNo_rinv y Hy (from left to right).
We will prove 0 = 0.
Use reflexivity.
An exact proof term for the current goal is add_SNo_cancel_L (x + y) (- (x + y)) ((- x) + (- y)) Lxy (SNo_minus_SNo (x + y) Lxy) (SNo_add_SNo (- x) (- y) Lmx Lmy) L1.
∎