Let x, y and z be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume _ _ _.
Assume _.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume _ _.
Assume _ _.
Apply SNoLtE y z Hy Hz Hyz to the current goal.
Let w be given.
Assume _ _.
Assume _ _.
Assume Hw2y Hw2z.
We will
prove x + y < x + z.
We will
prove x + y < x + w.
Apply H2 to the current goal.
We will
prove w ∈ SNoR y.
Apply SNoR_I y Hy w Hw1 to the current goal.
An exact proof term for the current goal is Hw2y.
An exact proof term for the current goal is Hw5.
We will
prove x + w < x + z.
Apply H4 to the current goal.
We will
prove w ∈ SNoL z.
Apply SNoL_I z Hz w Hw1 to the current goal.
An exact proof term for the current goal is Hw2z.
An exact proof term for the current goal is Hw6.
Assume _ _.
We will
prove x + y < x + z.
Apply H4 to the current goal.
We will
prove y ∈ SNoL z.
Apply SNoL_I z Hz y Hy to the current goal.
An exact proof term for the current goal is Hyz1.
An exact proof term for the current goal is Hyz.
Assume _ _.
We will
prove x + y < x + z.
Apply H2 to the current goal.
We will
prove z ∈ SNoR y.
Apply SNoR_I y Hy z Hz to the current goal.
An exact proof term for the current goal is Hzy.
An exact proof term for the current goal is Hyz.
∎