Let x, y and z be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hz: SNo z.
Assume Hxz: x < z.
Apply add_SNo_prop1 x y Hx Hy 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 H.
Apply H to the current goal.
Assume H1: SNo (x + y).
Assume _.
Assume H2: ∀u ∈ SNoR x, x + y < u + y.
Assume _ _ _.
Apply add_SNo_prop1 z y Hz Hy 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 H.
Apply H to the current goal.
Assume H3: SNo (z + y).
Assume H4: ∀u ∈ SNoL z, u + y < z + y.
Assume _ _ _ _.
Apply SNoLtE x z Hx Hz Hxz to the current goal.
Let w be given.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x ∩ SNoLev z.
Assume _ _.
Assume Hw5: x < w.
Assume Hw6: w < z.
Assume _ _.
Apply binintersectE (SNoLev x) (SNoLev z) (SNoLev w) Hw2 to the current goal.
Assume Hw2x Hw2z.
We will prove x + y < z + y.
Apply SNoLt_tra (x + y) (w + y) (z + y) H1 (SNo_add_SNo w y Hw1 Hy) H3 to the current goal.
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.
We will prove SNoLev w ∈ SNoLev x.
An exact proof term for the current goal is Hw2x.
We will prove x < w.
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.
We will prove SNoLev w ∈ SNoLev z.
An exact proof term for the current goal is Hw2z.
We will prove w < z.
An exact proof term for the current goal is Hw6.
Assume Hxz1: SNoLev x ∈ SNoLev z.
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.
We will prove SNoLev x ∈ SNoLev z.
An exact proof term for the current goal is Hxz1.
We will prove x < z.
An exact proof term for the current goal is Hxz.
Assume Hzx: SNoLev z ∈ SNoLev x.
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.
We will prove SNoLev z ∈ SNoLev x.
An exact proof term for the current goal is Hzx.
We will prove x < z.
An exact proof term for the current goal is Hxz.
∎