Let x and y be given.

Assume Hx Hy.

Let n be given.

Assume Hn.

Assume Hxy.

Apply SNoLt_tra x y (y + eps_ n) Hx Hy (SNo_add_SNo y (eps_ n) Hy (SNo_eps_ n Hn)) Hxy to the current goal.

We will prove y < y + eps_ n.

An exact proof term for the current goal is add_SNo_eps_Lt y Hy n Hn.

∎