Let x, y and z be given.

Assume Hx Hy Hz H1.

Apply SNoLeE z (x + - y) Hz (SNo_add_SNo x (- y) Hx (SNo_minus_SNo y Hy)) H1 to the current goal.

Assume H2.

Apply SNoLtLe to the current goal.

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

Assume H2: z = x + - y.

We will prove z + y ≤ x.

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

We will prove (x + - y) + y ≤ x.

rewrite the current goal using add_SNo_minus_R2' x y Hx Hy (from left to right).

Apply SNoLe_ref to the current goal.

∎