Let x, y and z be given.
Assume Hx Hy Hz H1.
We will prove x < z.
We prove the intermediate claim L1: (x + y) + - y = x.
An exact proof term for the current goal is add_SNo_minus_R2 x y Hx Hy.
We prove the intermediate claim L2: (z + y) + - y = z.
An exact proof term for the current goal is add_SNo_minus_R2 z y Hz Hy.
rewrite the current goal using L1 (from right to left).
rewrite the current goal using L2 (from right to left).
We will prove (x + y) + - y < (z + y) + - y.
An exact proof term for the current goal is add_SNo_Lt1 (x + y) (- y) (z + y) (SNo_add_SNo x y Hx Hy) (SNo_minus_SNo y Hy) (SNo_add_SNo z y Hz Hy) H1.
∎