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