Let u be given.
Apply SNoL_E (- x) Lmx u Hu to the current goal.
We prove the intermediate
claim Lmu:
SNo (- u).
An exact proof term for the current goal is Hu1.
We prove the intermediate
claim Lmuu:
- u + u = 0.
Apply IH to the current goal.
Apply SNoS_I2 u x Hu1 Hx to the current goal.
rewrite the current goal using
minus_SNo_Lev x Hx (from right to left).
An exact proof term for the current goal is Hu2.
We prove the intermediate
claim Lxmu:
x < - u.
We will
prove - - x < - u.
An exact proof term for the current goal is Hu3.
rewrite the current goal using Hwu (from left to right).
rewrite the current goal using
add_SNo_com u x Hu1 Hx (from left to right).
rewrite the current goal using Lmuu (from right to left).
We will
prove x + u < - u + u.
An exact proof term for the current goal is Lxmu.
Let u be given.
Apply SNoL_E x Hx u Hu to the current goal.
We prove the intermediate
claim Lmu:
SNo (- u).
An exact proof term for the current goal is Hu1.
We prove the intermediate
claim Lmuu:
- u + u = 0.
Apply IH to the current goal.
Apply SNoS_I2 u x Hu1 Hx to the current goal.
An exact proof term for the current goal is Hu2.
We prove the intermediate
claim Lmxmu:
- x < - u.
An exact proof term for the current goal is Hu3.
rewrite the current goal using Hwu (from left to right).
We will
prove - x + u < 0.
rewrite the current goal using Lmuu (from right to left).
We will
prove - x + u < - u + u.
An exact proof term for the current goal is Lmxmu.