Let x be given.

Assume HxS: SNo x.

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

We prove the intermediate claim Hadd: add_SNo x 0 = x.

An exact proof term for the current goal is (add_SNo_0R x HxS).

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

Use reflexivity.

∎