Let x, y and z be given.
Assume Hx Hy Hz Hxy Hyxz.
We prove the intermediate
claim L1:
0 ≤ y + - x.
rewrite the current goal using add_SNo_minus_SNo_rinv x Hx (from right to left).
We will
prove x + - x ≤ y + - x.
An
exact proof term for the current goal is
add_SNo_Le1 x (- x) y Hx (SNo_minus_SNo x Hx) Hy Hxy.
We prove the intermediate
claim L2:
abs_SNo (y + - x) = y + - x.
Apply nonneg_abs_SNo (y + - x) L1 to the current goal.
rewrite the current goal using L2 (from left to right).
We will
prove y + - x < z.
Apply add_SNo_minus_Lt1b y x z Hy Hx Hz to the current goal.
rewrite the current goal using add_SNo_com z x Hz Hx (from left to right).
An exact proof term for the current goal is Hyxz.
∎