Let x, y and z be given.
Assume Hx Hy Hz H1.
Apply SNoLeE (z + y) x (SNo_add_SNo z y Hz Hy) Hx 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_Lt2b x y z Hx Hy Hz H2.
Assume H2: z + y = x.
We will prove z ≤ x + - y.
rewrite the current goal using H2 (from right to left).
We will prove z ≤ (z + y) + - y.
rewrite the current goal using add_SNo_minus_R2 z y Hz Hy (from left to right).
Apply SNoLe_ref to the current goal.
∎