Let x be given.

Assume Hx.

Let n be given.

Assume Hn.

rewrite the current goal using add_SNo_0R x Hx (from right to left) at position 1.

We will prove x + 0 < x + eps_ n.

Apply add_SNo_Lt2 x 0 (eps_ n) Hx SNo_0 (SNo_eps_ n Hn) to the current goal.

An exact proof term for the current goal is SNo_eps_pos n Hn.

∎