Let x, y and z be given.

Assume Hx: SNo x.

Assume Hy: SNo y.

Assume Hz: SNo z.

Assume Hyz: y ≤ z.

We will prove x + y ≤ x + z.

Apply SNoLeE y z Hy Hz Hyz to the current goal.

Assume H1: y < z.

Apply SNoLtLe to the current goal.

An exact proof term for the current goal is add_SNo_Lt2 x y z Hx Hy Hz H1.

Assume H1: y = z.

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

Apply SNoLe_ref to the current goal.

∎