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 _ _ _ _.
Apply SNoLtE x z Hx Hz Hxz to the current goal.
Let w be given.
Assume _ _.
Assume _ _.
Assume Hw2x Hw2z.
We will
prove x + y < z + y.
We will
prove x + y < w + y.
Apply H2 to the current goal.
We will
prove w ∈ SNoR x.
Apply SNoR_I x Hx w Hw1 to the current goal.
An exact proof term for the current goal is Hw2x.
An exact proof term for the current goal is Hw5.
We will
prove w + y < z + y.
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 < z + y.
Apply H4 to the current goal.
We will
prove x ∈ SNoL z.
Apply SNoL_I z Hz x Hx to the current goal.
An exact proof term for the current goal is Hxz1.
An exact proof term for the current goal is Hxz.
Assume _ _.
We will
prove x + y < z + y.
Apply H2 to the current goal.
We will
prove z ∈ SNoR x.
Apply SNoR_I x Hx z Hz to the current goal.
An exact proof term for the current goal is Hzx.
An exact proof term for the current goal is Hxz.
∎