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.
We prove the intermediate claim L1: - x + (x + y) = y.
rewrite the current goal using add_SNo_assoc (- x) x y Lmx Hx Hy (from left to right).
We will prove (- x + x) + y = y.
rewrite the current goal using add_SNo_minus_SNo_linv x Hx (from left to right).
We will prove 0 + y = y.
An exact proof term for the current goal is add_SNo_0L y Hy.
We prove the intermediate claim L2: - x + (x + z) = z.
rewrite the current goal using add_SNo_assoc (- x) x z Lmx Hx Hz (from left to right).
We will prove (- x + x) + z = z.
rewrite the current goal using add_SNo_minus_SNo_linv x Hx (from left to right).
We will prove 0 + z = z.
An exact proof term for the current goal is add_SNo_0L z Hz.
rewrite the current goal using L1 (from right to left).
rewrite the current goal using Hxyz (from left to right).
An exact proof term for the current goal is L2.
∎