Set P to be the term λx y z ⇒ x + (y + z) = (x + y) + z of type set → set → set → prop.
Apply SNoLev_ind3 to the current goal.
Let x, y and z be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hz: SNo z.
Assume IH1: ∀u ∈ SNoS_ (SNoLev x), P u y z.
Assume IH2: ∀v ∈ SNoS_ (SNoLev y), P x v z.
Assume IH3: ∀w ∈ SNoS_ (SNoLev z), P x y w.
Assume IH4: ∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), P u v z.
Assume IH5: ∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), P u y w.
Assume IH6: ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P x v w.
Assume IH7: ∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P u v w.
We will prove x + (y + z) = (x + y) + z.
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx Hy.
We prove the intermediate claim Lyz: SNo (y + z).
An exact proof term for the current goal is SNo_add_SNo y z Hy Hz.
Set Lxyz1 to be the term {w + (y + z)|w ∈ SNoL x}.
Set Lxyz2 to be the term {x + w|w ∈ SNoL (y + z)}.
Set Rxyz1 to be the term {w + (y + z)|w ∈ SNoR x}.
Set Rxyz2 to be the term {x + w|w ∈ SNoR (y + z)}.
Set Lxyz3 to be the term {w + z|w ∈ SNoL (x + y)}.
Set Lxyz4 to be the term {(x + y) + w|w ∈ SNoL z}.
Set Rxyz3 to be the term {w + z|w ∈ SNoR (x + y)}.
Set Rxyz4 to be the term {(x + y) + w|w ∈ SNoR z}.
rewrite the current goal using add_SNo_eq x Hx (y + z) Lyz (from left to right).
rewrite the current goal using add_SNo_eq (x + y) Lxy z Hz (from left to right).
We will prove (SNoCut (Lxyz1 ∪ Lxyz2) (Rxyz1 ∪ Rxyz2)) = (SNoCut (Lxyz3 ∪ Lxyz4) (Rxyz3 ∪ Rxyz4)).
We prove the intermediate claim Lxyz12: SNoCutP (Lxyz1 ∪ Lxyz2) (Rxyz1 ∪ Rxyz2).
An exact proof term for the current goal is add_SNo_SNoCutP x (y + z) Hx Lyz.
We prove the intermediate claim Lxyz34: SNoCutP (Lxyz3 ∪ Lxyz4) (Rxyz3 ∪ Rxyz4).
An exact proof term for the current goal is add_SNo_SNoCutP (x + y) z Lxy Hz.
Apply SNoCut_ext to the current goal.
An exact proof term for the current goal is Lxyz12.
An exact proof term for the current goal is Lxyz34.
We will prove ∀w ∈ Lxyz1 ∪ Lxyz2, w < SNoCut (Lxyz3 ∪ Lxyz4) (Rxyz3 ∪ Rxyz4).
rewrite the current goal using add_SNo_eq (x + y) Lxy z Hz (from right to left).
We will prove ∀w ∈ Lxyz1 ∪ Lxyz2, w < (x + y) + z.
Let w be given.
Assume Hw: w ∈ Lxyz1 ∪ Lxyz2.
Apply binunionE Lxyz1 Lxyz2 w Hw to the current goal.
Assume Hw: w ∈ Lxyz1.
Apply ReplE_impred (SNoL x) (λw ⇒ w + (y + z)) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Assume Hwu: w = u + (y + z).
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: u < x.
We will prove w < (x + y) + z.
rewrite the current goal using Hwu (from left to right).
We will prove u + (y + z) < (x + y) + z.
We prove the intermediate claim IH1u: u + (y + z) = (u + y) + z.
An exact proof term for the current goal is IH1 u (SNoL_SNoS_ x u Hu).
rewrite the current goal using IH1u (from left to right).
We will prove (u + y) + z < (x + y) + z.
Apply add_SNo_Lt1 (u + y) z (x + y) (SNo_add_SNo u y Hu1 Hy) Hz Lxy to the current goal.
We will prove u + y < x + y.
Apply add_SNo_Lt1 u y x Hu1 Hy Hx to the current goal.
We will prove u < x.
An exact proof term for the current goal is Hu3.
Assume Hw: w ∈ Lxyz2.
Apply ReplE_impred (SNoL (y + z)) (λw ⇒ x + w) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL (y + z).
Assume Hwu: w = x + u.
Apply SNoL_E (y + z) Lyz u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (y + z).
Assume Hu3: u < y + z.
rewrite the current goal using Hwu (from left to right).
We will prove x + u < (x + y) + z.
Apply add_SNo_SNoL_interpolate y z Hy Hz u Hu to the current goal.
Assume H1: ∃v ∈ SNoL y, u ≤ v + z.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoL y.
Assume H2: u ≤ v + z.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev y.
Assume Hv3: v < y.
We prove the intermediate claim IH2v: x + (v + z) = (x + v) + z.
An exact proof term for the current goal is IH2 v (SNoL_SNoS_ y v Hv).
We will prove x + u < (x + y) + z.
Apply SNoLeLt_tra (x + u) (x + (v + z)) ((x + y) + z) (SNo_add_SNo x u Hx Hu1) (SNo_add_SNo x (v + z) Hx (SNo_add_SNo v z Hv1 Hz)) (SNo_add_SNo (x + y) z Lxy Hz) to the current goal.
We will prove x + u ≤ x + (v + z).
Apply add_SNo_Le2 x u (v + z) Hx Hu1 (SNo_add_SNo v z Hv1 Hz) to the current goal.
We will prove u ≤ v + z.
An exact proof term for the current goal is H2.
We will prove x + (v + z) < (x + y) + z.
rewrite the current goal using IH2v (from left to right).
We will prove (x + v) + z < (x + y) + z.
Apply add_SNo_Lt1 (x + v) z (x + y) (SNo_add_SNo x v Hx Hv1) Hz Lxy to the current goal.
We will prove x + v < x + y.
Apply add_SNo_Lt2 x v y Hx Hv1 Hy to the current goal.
We will prove v < y.
An exact proof term for the current goal is Hv3.
Assume H1: ∃v ∈ SNoL z, u ≤ y + v.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoL z.
Assume H2: u ≤ y + v.
Apply SNoL_E z Hz v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev z.
Assume Hv3: v < z.
We prove the intermediate claim IH3v: x + (y + v) = (x + y) + v.
An exact proof term for the current goal is IH3 v (SNoL_SNoS_ z v Hv).
We will prove x + u < (x + y) + z.
Apply SNoLeLt_tra (x + u) (x + (y + v)) ((x + y) + z) (SNo_add_SNo x u Hx Hu1) (SNo_add_SNo x (y + v) Hx (SNo_add_SNo y v Hy Hv1)) (SNo_add_SNo (x + y) z Lxy Hz) to the current goal.
We will prove x + u ≤ x + (y + v).
Apply add_SNo_Le2 x u (y + v) Hx Hu1 (SNo_add_SNo y v Hy Hv1) to the current goal.
We will prove u ≤ y + v.
An exact proof term for the current goal is H2.
We will prove x + (y + v) < (x + y) + z.
rewrite the current goal using IH3v (from left to right).
We will prove (x + y) + v < (x + y) + z.
Apply add_SNo_Lt2 (x + y) v z Lxy Hv1 Hz to the current goal.
We will prove v < z.
An exact proof term for the current goal is Hv3.
We will prove ∀v ∈ Rxyz1 ∪ Rxyz2, SNoCut (Lxyz3 ∪ Lxyz4) (Rxyz3 ∪ Rxyz4) < v.
rewrite the current goal using add_SNo_eq (x + y) Lxy z Hz (from right to left).
We will prove ∀v ∈ Rxyz1 ∪ Rxyz2, (x + y) + z < v.
Let v be given.
Assume Hv: v ∈ Rxyz1 ∪ Rxyz2.
Apply binunionE Rxyz1 Rxyz2 v Hv to the current goal.
Assume Hv: v ∈ Rxyz1.
Apply ReplE_impred (SNoR x) (λw ⇒ w + (y + z)) v Hv to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR x.
Assume Hvu: v = u + (y + z).
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: x < u.
We will prove (x + y) + z < v.
rewrite the current goal using Hvu (from left to right).
We will prove (x + y) + z < u + (y + z).
We prove the intermediate claim IH1u: u + (y + z) = (u + y) + z.
An exact proof term for the current goal is IH1 u (SNoR_SNoS_ x u Hu).
rewrite the current goal using IH1u (from left to right).
We will prove (x + y) + z < (u + y) + z.
Apply add_SNo_Lt1 (x + y) z (u + y) Lxy Hz (SNo_add_SNo u y Hu1 Hy) to the current goal.
We will prove x + y < u + y.
Apply add_SNo_Lt1 x y u Hx Hy Hu1 to the current goal.
We will prove x < u.
An exact proof term for the current goal is Hu3.
Assume Hv: v ∈ Rxyz2.
Apply ReplE_impred (SNoR (y + z)) (λw ⇒ x + w) v Hv to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR (y + z).
Assume Hvu: v = x + u.
Apply SNoR_E (y + z) Lyz u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (y + z).
Assume Hu3: y + z < u.
rewrite the current goal using Hvu (from left to right).
We will prove (x + y) + z < x + u.
Apply add_SNo_SNoR_interpolate y z Hy Hz u Hu to the current goal.
Assume H1: ∃v ∈ SNoR y, v + z ≤ u.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoR y.
Assume H2: v + z ≤ u.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev y.
Assume Hv3: y < v.
We prove the intermediate claim IH2v: x + (v + z) = (x + v) + z.
An exact proof term for the current goal is IH2 v (SNoR_SNoS_ y v Hv).
We will prove (x + y) + z < x + u.
Apply SNoLtLe_tra ((x + y) + z) (x + (v + z)) (x + u) (SNo_add_SNo (x + y) z Lxy Hz) (SNo_add_SNo x (v + z) Hx (SNo_add_SNo v z Hv1 Hz)) (SNo_add_SNo x u Hx Hu1) to the current goal.
We will prove (x + y) + z < x + (v + z).
rewrite the current goal using IH2v (from left to right).
We will prove (x + y) + z < (x + v) + z.
Apply add_SNo_Lt1 (x + y) z (x + v) Lxy Hz (SNo_add_SNo x v Hx Hv1) to the current goal.
We will prove x + y < x + v.
Apply add_SNo_Lt2 x y v Hx Hy Hv1 to the current goal.
We will prove y < v.
An exact proof term for the current goal is Hv3.
We will prove x + (v + z) ≤ x + u.
Apply add_SNo_Le2 x (v + z) u Hx (SNo_add_SNo v z Hv1 Hz) Hu1 to the current goal.
We will prove v + z ≤ u.
An exact proof term for the current goal is H2.
Assume H1: ∃v ∈ SNoR z, y + v ≤ u.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoR z.
Assume H2: y + v ≤ u.
Apply SNoR_E z Hz v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev z.
Assume Hv3: z < v.
We prove the intermediate claim IH3v: x + (y + v) = (x + y) + v.
An exact proof term for the current goal is IH3 v (SNoR_SNoS_ z v Hv).
We will prove (x + y) + z < x + u.
Apply SNoLtLe_tra ((x + y) + z) (x + (y + v)) (x + u) (SNo_add_SNo (x + y) z Lxy Hz) (SNo_add_SNo x (y + v) Hx (SNo_add_SNo y v Hy Hv1)) (SNo_add_SNo x u Hx Hu1) to the current goal.
We will prove (x + y) + z < x + (y + v).
rewrite the current goal using IH3v (from left to right).
We will prove (x + y) + z < (x + y) + v.
Apply add_SNo_Lt2 (x + y) z v Lxy Hz Hv1 to the current goal.
We will prove z < v.
An exact proof term for the current goal is Hv3.
We will prove x + (y + v) ≤ x + u.
Apply add_SNo_Le2 x (y + v) u Hx (SNo_add_SNo y v Hy Hv1) Hu1 to the current goal.
We will prove y + v ≤ u.
An exact proof term for the current goal is H2.
We will prove ∀w ∈ Lxyz3 ∪ Lxyz4, w < SNoCut (Lxyz1 ∪ Lxyz2) (Rxyz1 ∪ Rxyz2).
rewrite the current goal using add_SNo_eq x Hx (y + z) Lyz (from right to left).
We will prove ∀w ∈ Lxyz3 ∪ Lxyz4, w < x + (y + z).
Let w be given.
Assume Hw: w ∈ Lxyz3 ∪ Lxyz4.
Apply binunionE Lxyz3 Lxyz4 w Hw to the current goal.
Assume Hw: w ∈ Lxyz3.
Apply ReplE_impred (SNoL (x + y)) (λw ⇒ w + z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL (x + y).
Assume Hwu: w = u + z.
Apply SNoL_E (x + y) Lxy u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: u < x + y.
rewrite the current goal using Hwu (from left to right).
We will prove u + z < x + (y + z).
Apply add_SNo_SNoL_interpolate x y Hx Hy u Hu to the current goal.
Assume H1: ∃v ∈ SNoL x, u ≤ v + y.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoL x.
Assume H2: u ≤ v + y.
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: v < x.
We prove the intermediate claim IH1v: v + (y + z) = (v + y) + z.
An exact proof term for the current goal is IH1 v (SNoL_SNoS_ x v Hv).
We will prove u + z < x + (y + z).
Apply SNoLeLt_tra (u + z) ((v + y) + z) (x + (y + z)) (SNo_add_SNo u z Hu1 Hz) (SNo_add_SNo (v + y) z (SNo_add_SNo v y Hv1 Hy) Hz) (SNo_add_SNo x (y + z) Hx Lyz) to the current goal.
We will prove u + z ≤ (v + y) + z.
Apply add_SNo_Le1 u z (v + y) Hu1 Hz (SNo_add_SNo v y Hv1 Hy) to the current goal.
We will prove u ≤ v + y.
An exact proof term for the current goal is H2.
We will prove (v + y) + z < x + (y + z).
rewrite the current goal using IH1v (from right to left).
We will prove v + (y + z) < x + (y + z).
Apply add_SNo_Lt1 v (y + z) x Hv1 Lyz Hx to the current goal.
We will prove v < x.
An exact proof term for the current goal is Hv3.
Assume H1: ∃v ∈ SNoL y, u ≤ x + v.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoL y.
Assume H2: u ≤ x + v.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev y.
Assume Hv3: v < y.
We prove the intermediate claim IH2v: x + (v + z) = (x + v) + z.
An exact proof term for the current goal is IH2 v (SNoL_SNoS_ y v Hv).
We will prove u + z < x + (y + z).
Apply SNoLeLt_tra (u + z) ((x + v) + z) (x + (y + z)) (SNo_add_SNo u z Hu1 Hz) (SNo_add_SNo (x + v) z (SNo_add_SNo x v Hx Hv1) Hz) (SNo_add_SNo x (y + z) Hx Lyz) to the current goal.
We will prove u + z ≤ (x + v) + z.
Apply add_SNo_Le1 u z (x + v) Hu1 Hz (SNo_add_SNo x v Hx Hv1) to the current goal.
We will prove u ≤ x + v.
An exact proof term for the current goal is H2.
We will prove (x + v) + z < x + (y + z).
rewrite the current goal using IH2v (from right to left).
We will prove x + (v + z) < x + (y + z).
Apply add_SNo_Lt2 x (v + z) (y + z) Hx (SNo_add_SNo v z Hv1 Hz) Lyz to the current goal.
We will prove v + z < y + z.
Apply add_SNo_Lt1 v z y Hv1 Hz Hy to the current goal.
We will prove v < y.
An exact proof term for the current goal is Hv3.
Assume Hw: w ∈ Lxyz4.
Apply ReplE_impred (SNoL z) (λw ⇒ (x + y) + w) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL z.
Assume Hwu: w = (x + y) + u.
Apply SNoL_E z Hz u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev z.
Assume Hu3: u < z.
We will prove w < x + (y + z).
rewrite the current goal using Hwu (from left to right).
We will prove (x + y) + u < x + (y + z).
We prove the intermediate claim IH3u: x + (y + u) = (x + y) + u.
An exact proof term for the current goal is IH3 u (SNoL_SNoS_ z u Hu).
rewrite the current goal using IH3u (from right to left).
We will prove x + (y + u) < x + (y + z).
Apply add_SNo_Lt2 x (y + u) (y + z) Hx (SNo_add_SNo y u Hy Hu1) Lyz to the current goal.
We will prove y + u < y + z.
Apply add_SNo_Lt2 y u z Hy Hu1 Hz to the current goal.
We will prove u < z.
An exact proof term for the current goal is Hu3.
We will prove ∀v ∈ Rxyz3 ∪ Rxyz4, SNoCut (Lxyz1 ∪ Lxyz2) (Rxyz1 ∪ Rxyz2) < v.
rewrite the current goal using add_SNo_eq x Hx (y + z) Lyz (from right to left).
We will prove ∀v ∈ Rxyz3 ∪ Rxyz4, x + (y + z) < v.
Let v be given.
Assume Hv: v ∈ Rxyz3 ∪ Rxyz4.
Apply binunionE Rxyz3 Rxyz4 v Hv to the current goal.
Assume Hv: v ∈ Rxyz3.
Apply ReplE_impred (SNoR (x + y)) (λw ⇒ w + z) v Hv to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR (x + y).
Assume Hvu: v = u + z.
Apply SNoR_E (x + y) Lxy u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: x + y < u.
rewrite the current goal using Hvu (from left to right).
We will prove x + (y + z) < u + z.
Apply add_SNo_SNoR_interpolate x y Hx Hy u Hu to the current goal.
Assume H1: ∃v ∈ SNoR x, v + y ≤ u.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoR x.
Assume H2: v + y ≤ u.
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: x < v.
We prove the intermediate claim IH1v: v + (y + z) = (v + y) + z.
An exact proof term for the current goal is IH1 v (SNoR_SNoS_ x v Hv).
We will prove x + (y + z) < u + z.
Apply SNoLtLe_tra (x + (y + z)) ((v + y) + z) (u + z) (SNo_add_SNo x (y + z) Hx Lyz) (SNo_add_SNo (v + y) z (SNo_add_SNo v y Hv1 Hy) Hz) (SNo_add_SNo u z Hu1 Hz) to the current goal.
We will prove x + (y + z) < (v + y) + z.
rewrite the current goal using IH1v (from right to left).
We will prove x + (y + z) < v + (y + z).
Apply add_SNo_Lt1 x (y + z) v Hx Lyz Hv1 to the current goal.
We will prove x < v.
An exact proof term for the current goal is Hv3.
We will prove (v + y) + z ≤ u + z.
Apply add_SNo_Le1 (v + y) z u (SNo_add_SNo v y Hv1 Hy) Hz Hu1 to the current goal.
We will prove v + y ≤ u.
An exact proof term for the current goal is H2.
Assume H1: ∃v ∈ SNoR y, x + v ≤ u.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoR y.
Assume H2: x + v ≤ u.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev y.
Assume Hv3: y < v.
We prove the intermediate claim IH2v: x + (v + z) = (x + v) + z.
An exact proof term for the current goal is IH2 v (SNoR_SNoS_ y v Hv).
We will prove x + (y + z) < u + z.
Apply SNoLtLe_tra (x + (y + z)) ((x + v) + z) (u + z) (SNo_add_SNo x (y + z) Hx Lyz) (SNo_add_SNo (x + v) z (SNo_add_SNo x v Hx Hv1) Hz) (SNo_add_SNo u z Hu1 Hz) to the current goal.
We will prove x + (y + z) < (x + v) + z.
rewrite the current goal using IH2v (from right to left).
We will prove x + (y + z) < x + (v + z).
Apply add_SNo_Lt2 x (y + z) (v + z) Hx Lyz (SNo_add_SNo v z Hv1 Hz) to the current goal.
We will prove y + z < v + z.
Apply add_SNo_Lt1 y z v Hy Hz Hv1 to the current goal.
We will prove y < v.
An exact proof term for the current goal is Hv3.
We will prove (x + v) + z ≤ u + z.
Apply add_SNo_Le1 (x + v) z u (SNo_add_SNo x v Hx Hv1) Hz Hu1 to the current goal.
We will prove x + v ≤ u.
An exact proof term for the current goal is H2.
Assume Hv: v ∈ Rxyz4.
Apply ReplE_impred (SNoR z) (λw ⇒ (x + y) + w) v Hv to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR z.
Assume Hvu: v = (x + y) + u.
Apply SNoR_E z Hz u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev z.
Assume Hu3: z < u.
We will prove x + (y + z) < v.
rewrite the current goal using Hvu (from left to right).
We will prove x + (y + z) < (x + y) + u.
We prove the intermediate claim IH3u: x + (y + u) = (x + y) + u.
An exact proof term for the current goal is IH3 u (SNoR_SNoS_ z u Hu).
rewrite the current goal using IH3u (from right to left).
We will prove x + (y + z) < x + (y + u).
Apply add_SNo_Lt2 x (y + z) (y + u) Hx Lyz (SNo_add_SNo y u Hy Hu1) to the current goal.
We will prove y + z < y + u.
Apply add_SNo_Lt2 y z u Hy Hz Hu1 to the current goal.
We will prove z < u.
An exact proof term for the current goal is Hu3.
∎