Let Lx, Rx, Ly, Ry, x and y be given.
Assume HLRx HLRy Hxe Hye.
Apply HLRx to the current goal.
Assume H.
Apply H to the current goal.
Assume HLRx1: ∀w ∈ Lx, SNo w.
Assume HLRx2: ∀z ∈ Rx, SNo z.
Assume HLRx3: ∀w ∈ Lx, ∀z ∈ Rx, w < z.
Apply HLRy to the current goal.
Assume H.
Apply H to the current goal.
Assume HLRy1: ∀w ∈ Ly, SNo w.
Assume HLRy2: ∀z ∈ Ry, SNo z.
Assume HLRy3: ∀w ∈ Ly, ∀z ∈ Ry, w < z.
Set Lx' to be the term {w + y|w ∈ Lx}.
Set Ly' to be the term {x + w|w ∈ Ly}.
Set Rx' to be the term {z + y|z ∈ Rx}.
Set Ry' to be the term {x + z|z ∈ Ry}.
Apply SNoCutP_SNoCut_impred Lx Rx HLRx to the current goal.
rewrite the current goal using Hxe (from right to left).
Assume Hx1: SNo x.
Assume Hx2: SNoLev x ∈ ordsucc ((⋃w ∈ Lxordsucc (SNoLev w)) ∪ (⋃z ∈ Rxordsucc (SNoLev z))).
Assume Hx3: ∀w ∈ Lx, w < x.
Assume Hx4: ∀z ∈ Rx, x < z.
Assume Hx5: (∀u, SNo u → (∀w ∈ Lx, w < u) → (∀z ∈ Rx, u < z) → SNoLev x ⊆ SNoLev u ∧ SNoEq_ (SNoLev x) x u).
Apply SNoCutP_SNoCut_impred Ly Ry HLRy to the current goal.
rewrite the current goal using Hye (from right to left).
Assume Hy1: SNo y.
Assume Hy2: SNoLev y ∈ ordsucc ((⋃w ∈ Lyordsucc (SNoLev w)) ∪ (⋃z ∈ Ryordsucc (SNoLev z))).
Assume Hy3: ∀w ∈ Ly, w < y.
Assume Hy4: ∀z ∈ Ry, y < z.
Assume Hy5: (∀u, SNo u → (∀w ∈ Ly, w < u) → (∀z ∈ Ry, u < z) → SNoLev y ⊆ SNoLev u ∧ SNoEq_ (SNoLev y) y u).
We prove the intermediate claim L1: SNoCutP (Lx' ∪ Ly') (Rx' ∪ Ry').
We will prove (∀w ∈ Lx' ∪ Ly', SNo w) ∧ (∀z ∈ Rx' ∪ Ry', SNo z) ∧ (∀w ∈ Lx' ∪ Ly', ∀z ∈ Rx' ∪ Ry', w < z).
Apply and3I to the current goal.
Let w be given.
Apply binunionE' to the current goal.
Assume Hw: w ∈ Lx'.
Apply ReplE_impred Lx (λw ⇒ w + y) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ Lx.
Assume Hwe: w = w' + y.
rewrite the current goal using Hwe (from left to right).
An exact proof term for the current goal is SNo_add_SNo w' y (HLRx1 w' Hw') Hy1.
Assume Hw: w ∈ Ly'.
Apply ReplE_impred Ly (λw ⇒ x + w) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ Ly.
Assume Hwe: w = x + w'.
rewrite the current goal using Hwe (from left to right).
An exact proof term for the current goal is SNo_add_SNo x w' Hx1 (HLRy1 w' Hw').
Let z be given.
Apply binunionE' to the current goal.
Assume Hz: z ∈ Rx'.
Apply ReplE_impred Rx (λz ⇒ z + y) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Rx.
Assume Hze: z = z' + y.
rewrite the current goal using Hze (from left to right).
An exact proof term for the current goal is SNo_add_SNo z' y (HLRx2 z' Hz') Hy1.
Assume Hz: z ∈ Ry'.
Apply ReplE_impred Ry (λz ⇒ x + z) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Ry.
Assume Hze: z = x + z'.
rewrite the current goal using Hze (from left to right).
An exact proof term for the current goal is SNo_add_SNo x z' Hx1 (HLRy2 z' Hz').
Let w be given.
Apply binunionE' to the current goal.
Assume Hw: w ∈ Lx'.
Apply ReplE_impred Lx (λw ⇒ w + y) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ Lx.
We prove the intermediate claim Lw': SNo w'.
An exact proof term for the current goal is HLRx1 w' Hw'.
Assume Hwe: w = w' + y.
rewrite the current goal using Hwe (from left to right).
Let z be given.
Apply binunionE' to the current goal.
Assume Hz: z ∈ Rx'.
Apply ReplE_impred Rx (λz ⇒ z + y) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Rx.
Assume Hze: z = z' + y.
We prove the intermediate claim Lz': SNo z'.
An exact proof term for the current goal is HLRx2 z' Hz'.
rewrite the current goal using Hze (from left to right).
We will prove w' + y < z' + y.
Apply add_SNo_Lt1 w' y z' Lw' Hy1 Lz' to the current goal.
We will prove w' < z'.
An exact proof term for the current goal is SNoLt_tra w' x z' Lw' Hx1 Lz' (Hx3 w' Hw') (Hx4 z' Hz').
Assume Hz: z ∈ Ry'.
Apply ReplE_impred Ry (λz ⇒ x + z) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Ry.
Assume Hze: z = x + z'.
We prove the intermediate claim Lz': SNo z'.
An exact proof term for the current goal is HLRy2 z' Hz'.
rewrite the current goal using Hze (from left to right).
We will prove w' + y < x + z'.
Apply add_SNo_Lt3 w' y x z' Lw' Hy1 Hx1 Lz' to the current goal.
We will prove w' < x.
An exact proof term for the current goal is Hx3 w' Hw'.
We will prove y < z'.
An exact proof term for the current goal is Hy4 z' Hz'.
Assume Hw: w ∈ Ly'.
Apply ReplE_impred Ly (λw ⇒ x + w) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ Ly.
Assume Hwe: w = x + w'.
We prove the intermediate claim Lw': SNo w'.
An exact proof term for the current goal is HLRy1 w' Hw'.
rewrite the current goal using Hwe (from left to right).
Let z be given.
Apply binunionE' to the current goal.
Assume Hz: z ∈ Rx'.
Apply ReplE_impred Rx (λz ⇒ z + y) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Rx.
Assume Hze: z = z' + y.
We prove the intermediate claim Lz': SNo z'.
An exact proof term for the current goal is HLRx2 z' Hz'.
rewrite the current goal using Hze (from left to right).
We will prove x + w' < z' + y.
Apply add_SNo_Lt3 x w' z' y Hx1 Lw' Lz' Hy1 to the current goal.
We will prove x < z'.
An exact proof term for the current goal is Hx4 z' Hz'.
We will prove w' < y.
An exact proof term for the current goal is Hy3 w' Hw'.
Assume Hz: z ∈ Ry'.
Apply ReplE_impred Ry (λz ⇒ x + z) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Ry.
Assume Hze: z = x + z'.
We prove the intermediate claim Lz': SNo z'.
An exact proof term for the current goal is HLRy2 z' Hz'.
rewrite the current goal using Hze (from left to right).
We will prove x + w' < x + z'.
Apply add_SNo_Lt2 x w' z' Hx1 Lw' Lz' to the current goal.
We will prove w' < z'.
An exact proof term for the current goal is SNoLt_tra w' y z' Lw' Hy1 Lz' (Hy3 w' Hw') (Hy4 z' Hz').
Apply andI (SNoCutP (Lx' ∪ Ly') (Rx' ∪ Ry')) (x + y = SNoCut (Lx' ∪ Ly') (Rx' ∪ Ry')) L1 to the current goal.
We will prove x + y = SNoCut (Lx' ∪ Ly') (Rx' ∪ Ry').
rewrite the current goal using add_SNo_eq x Hx1 y Hy1 (from left to right).
We will prove SNoCut ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y}) = SNoCut (Lx' ∪ Ly') (Rx' ∪ Ry').
Set v to be the term SNoCut (Lx' ∪ Ly') (Rx' ∪ Ry').
Apply SNoCutP_SNoCut_impred (Lx' ∪ Ly') (Rx' ∪ Ry') L1 to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ ordsucc ((⋃w ∈ Lx' ∪ Ly'ordsucc (SNoLev w)) ∪ (⋃z ∈ Rx' ∪ Ry'ordsucc (SNoLev z))).
Assume Hv3: ∀w ∈ Lx' ∪ Ly', w < v.
Assume Hv4: ∀z ∈ Rx' ∪ Ry', v < z.
Assume Hv5: ∀u, SNo u → (∀w ∈ Lx' ∪ Ly', w < u) → (∀z ∈ Rx' ∪ Ry', u < z) → SNoLev v ⊆ SNoLev u ∧ SNoEq_ (SNoLev v) v u.
Apply SNoCut_ext ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y}) (Lx' ∪ Ly') (Rx' ∪ Ry') to the current goal.
An exact proof term for the current goal is add_SNo_SNoCutP x y Hx1 Hy1.
An exact proof term for the current goal is L1.
We will prove ∀w ∈ {w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}, w < v.
Let w be given.
Apply binunionE' to the current goal.
Assume Hw.
Apply ReplE_impred (SNoL x) (λw ⇒ w + y) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ SNoL x.
Assume Hwe: w = w' + y.
Apply SNoL_E x Hx1 w' Hw' to the current goal.
Assume Hw'1: SNo w'.
Assume Hw'2: SNoLev w' ∈ SNoLev x.
Assume Hw'3: w' < x.
We prove the intermediate claim L2: ∃w'' ∈ Lx, w' ≤ w''.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L2a: SNoLev x ⊆ SNoLev w' ∧ SNoEq_ (SNoLev x) x w'.
Apply Hx5 w' Hw'1 to the current goal.
We will prove ∀w'' ∈ Lx, w'' < w'.
Let w'' be given.
Assume Hw''1.
Apply SNoLtLe_or w'' w' (HLRx1 w'' Hw''1) Hw'1 to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume Hw''2: w' ≤ w''.
We will prove False.
Apply HC to the current goal.
We use w'' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw''1.
An exact proof term for the current goal is Hw''2.
We will prove ∀z ∈ Rx, w' < z.
Let z be given.
Assume Hz.
Apply SNoLt_tra w' x z Hw'1 Hx1 (HLRx2 z Hz) to the current goal.
We will prove w' < x.
An exact proof term for the current goal is Hw'3.
We will prove x < z.
An exact proof term for the current goal is Hx4 z Hz.
Apply L2a to the current goal.
Assume Hxw': SNoLev x ⊆ SNoLev w'.
Assume _.
Apply In_irref (SNoLev w') to the current goal.
We will prove SNoLev w' ∈ SNoLev w'.
Apply Hxw' to the current goal.
An exact proof term for the current goal is Hw'2.
Apply L2 to the current goal.
Let w'' be given.
Assume H.
Apply H to the current goal.
Assume Hw''1: w'' ∈ Lx.
Assume Hw''2: w' ≤ w''.
rewrite the current goal using Hwe (from left to right).
We will prove w' + y < v.
Apply SNoLeLt_tra (w' + y) (w'' + y) v (SNo_add_SNo w' y Hw'1 Hy1) (SNo_add_SNo w'' y (HLRx1 w'' Hw''1) Hy1) Hv1 to the current goal.
We will prove w' + y ≤ w'' + y.
Apply add_SNo_Le1 w' y w'' Hw'1 Hy1 (HLRx1 w'' Hw''1) to the current goal.
We will prove w' ≤ w''.
An exact proof term for the current goal is Hw''2.
We will prove w'' + y < v.
Apply Hv3 to the current goal.
We will prove w'' + y ∈ Lx' ∪ Ly'.
Apply binunionI1 to the current goal.
We will prove w'' + y ∈ Lx'.
An exact proof term for the current goal is ReplI Lx (λw ⇒ w + y) w'' Hw''1.
Assume Hw.
Apply ReplE_impred (SNoL y) (λw ⇒ x + w) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ SNoL y.
Assume Hwe: w = x + w'.
Apply SNoL_E y Hy1 w' Hw' to the current goal.
Assume Hw'1: SNo w'.
Assume Hw'2: SNoLev w' ∈ SNoLev y.
Assume Hw'3: w' < y.
We prove the intermediate claim L3: ∃w'' ∈ Ly, w' ≤ w''.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L3a: SNoLev y ⊆ SNoLev w' ∧ SNoEq_ (SNoLev y) y w'.
Apply Hy5 w' Hw'1 to the current goal.
We will prove ∀w'' ∈ Ly, w'' < w'.
Let w'' be given.
Assume Hw''1.
Apply SNoLtLe_or w'' w' (HLRy1 w'' Hw''1) Hw'1 to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume Hw''2: w' ≤ w''.
We will prove False.
Apply HC to the current goal.
We use w'' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw''1.
An exact proof term for the current goal is Hw''2.
We will prove ∀z ∈ Ry, w' < z.
Let z be given.
Assume Hz.
Apply SNoLt_tra w' y z Hw'1 Hy1 (HLRy2 z Hz) to the current goal.
We will prove w' < y.
An exact proof term for the current goal is Hw'3.
We will prove y < z.
An exact proof term for the current goal is Hy4 z Hz.
Apply L3a to the current goal.
Assume Hyw': SNoLev y ⊆ SNoLev w'.
Assume _.
Apply In_irref (SNoLev w') to the current goal.
We will prove SNoLev w' ∈ SNoLev w'.
Apply Hyw' to the current goal.
An exact proof term for the current goal is Hw'2.
Apply L3 to the current goal.
Let w'' be given.
Assume H.
Apply H to the current goal.
Assume Hw''1: w'' ∈ Ly.
Assume Hw''2: w' ≤ w''.
rewrite the current goal using Hwe (from left to right).
We will prove x + w' < v.
Apply SNoLeLt_tra (x + w') (x + w'') v (SNo_add_SNo x w' Hx1 Hw'1) (SNo_add_SNo x w'' Hx1 (HLRy1 w'' Hw''1)) Hv1 to the current goal.
We will prove x + w' ≤ x + w''.
Apply add_SNo_Le2 x w' w'' Hx1 Hw'1 (HLRy1 w'' Hw''1) to the current goal.
We will prove w' ≤ w''.
An exact proof term for the current goal is Hw''2.
We will prove x + w'' < v.
Apply Hv3 to the current goal.
We will prove x + w'' ∈ Lx' ∪ Ly'.
Apply binunionI2 to the current goal.
We will prove x + w'' ∈ Ly'.
An exact proof term for the current goal is ReplI Ly (λw ⇒ x + w) w'' Hw''1.
We will prove ∀z ∈ {z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y}, v < z.
Let z be given.
Apply binunionE' to the current goal.
Assume Hz.
Apply ReplE_impred (SNoR x) (λz ⇒ z + y) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ SNoR x.
Assume Hze: z = z' + y.
Apply SNoR_E x Hx1 z' Hz' to the current goal.
Assume Hz'1: SNo z'.
Assume Hz'2: SNoLev z' ∈ SNoLev x.
Assume Hz'3: x < z'.
We prove the intermediate claim L4: ∃z'' ∈ Rx, z'' ≤ z'.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L4a: SNoLev x ⊆ SNoLev z' ∧ SNoEq_ (SNoLev x) x z'.
Apply Hx5 z' Hz'1 to the current goal.
We will prove ∀w ∈ Lx, w < z'.
Let w be given.
Assume Hw.
Apply SNoLt_tra w x z' (HLRx1 w Hw) Hx1 Hz'1 to the current goal.
We will prove w < x.
An exact proof term for the current goal is Hx3 w Hw.
We will prove x < z'.
An exact proof term for the current goal is Hz'3.
We will prove ∀z'' ∈ Rx, z' < z''.
Let z'' be given.
Assume Hz''1.
Apply SNoLtLe_or z' z'' Hz'1 (HLRx2 z'' Hz''1) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume Hz''2: z'' ≤ z'.
We will prove False.
Apply HC to the current goal.
We use z'' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz''1.
An exact proof term for the current goal is Hz''2.
Apply L4a to the current goal.
Assume Hxz': SNoLev x ⊆ SNoLev z'.
Assume _.
Apply In_irref (SNoLev z') to the current goal.
We will prove SNoLev z' ∈ SNoLev z'.
Apply Hxz' to the current goal.
An exact proof term for the current goal is Hz'2.
Apply L4 to the current goal.
Let z'' be given.
Assume H.
Apply H to the current goal.
Assume Hz''1: z'' ∈ Rx.
Assume Hz''2: z'' ≤ z'.
rewrite the current goal using Hze (from left to right).
We will prove v < z' + y.
Apply SNoLtLe_tra v (z'' + y) (z' + y) Hv1 (SNo_add_SNo z'' y (HLRx2 z'' Hz''1) Hy1) (SNo_add_SNo z' y Hz'1 Hy1) to the current goal.
We will prove v < z'' + y.
Apply Hv4 to the current goal.
We will prove z'' + y ∈ Rx' ∪ Ry'.
Apply binunionI1 to the current goal.
We will prove z'' + y ∈ Rx'.
An exact proof term for the current goal is ReplI Rx (λz ⇒ z + y) z'' Hz''1.
We will prove z'' + y ≤ z' + y.
Apply add_SNo_Le1 z'' y z' (HLRx2 z'' Hz''1) Hy1 Hz'1 to the current goal.
We will prove z'' ≤ z'.
An exact proof term for the current goal is Hz''2.
Assume Hz.
Apply ReplE_impred (SNoR y) (λz ⇒ x + z) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ SNoR y.
Assume Hze: z = x + z'.
Apply SNoR_E y Hy1 z' Hz' to the current goal.
Assume Hz'1: SNo z'.
Assume Hz'2: SNoLev z' ∈ SNoLev y.
Assume Hz'3: y < z'.
We prove the intermediate claim L5: ∃z'' ∈ Ry, z'' ≤ z'.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L5a: SNoLev y ⊆ SNoLev z' ∧ SNoEq_ (SNoLev y) y z'.
Apply Hy5 z' Hz'1 to the current goal.
We will prove ∀w ∈ Ly, w < z'.
Let w be given.
Assume Hw.
Apply SNoLt_tra w y z' (HLRy1 w Hw) Hy1 Hz'1 to the current goal.
We will prove w < y.
An exact proof term for the current goal is Hy3 w Hw.
We will prove y < z'.
An exact proof term for the current goal is Hz'3.
We will prove ∀z'' ∈ Ry, z' < z''.
Let z'' be given.
Assume Hz''1.
Apply SNoLtLe_or z' z'' Hz'1 (HLRy2 z'' Hz''1) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume Hz''2: z'' ≤ z'.
We will prove False.
Apply HC to the current goal.
We use z'' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz''1.
An exact proof term for the current goal is Hz''2.
Apply L5a to the current goal.
Assume Hyz': SNoLev y ⊆ SNoLev z'.
Assume _.
Apply In_irref (SNoLev z') to the current goal.
We will prove SNoLev z' ∈ SNoLev z'.
Apply Hyz' to the current goal.
An exact proof term for the current goal is Hz'2.
Apply L5 to the current goal.
Let z'' be given.
Assume H.
Apply H to the current goal.
Assume Hz''1: z'' ∈ Ry.
Assume Hz''2: z'' ≤ z'.
rewrite the current goal using Hze (from left to right).
We will prove v < x + z'.
Apply SNoLtLe_tra v (x + z'') (x + z') Hv1 (SNo_add_SNo x z'' Hx1 (HLRy2 z'' Hz''1)) (SNo_add_SNo x z' Hx1 Hz'1) to the current goal.
We will prove v < x + z''.
Apply Hv4 to the current goal.
We will prove x + z'' ∈ Rx' ∪ Ry'.
Apply binunionI2 to the current goal.
We will prove x + z'' ∈ Ry'.
An exact proof term for the current goal is ReplI Ry (λz ⇒ x + z) z'' Hz''1.
We will prove x + z'' ≤ x + z'.
Apply add_SNo_Le2 x z'' z' Hx1 (HLRy2 z'' Hz''1) Hz'1 to the current goal.
We will prove z'' ≤ z'.
An exact proof term for the current goal is Hz''2.
rewrite the current goal using add_SNo_eq x Hx1 y Hy1 (from right to left).
We will prove ∀w ∈ Lx' ∪ Ly', w < x + y.
Let w be given.
Apply binunionE' to the current goal.
Assume Hw: w ∈ Lx'.
Apply ReplE_impred Lx (λw ⇒ w + y) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ Lx.
Assume Hwe: w = w' + y.
rewrite the current goal using Hwe (from left to right).
We will prove w' + y < x + y.
Apply add_SNo_Lt1 w' y x (HLRx1 w' Hw') Hy1 Hx1 to the current goal.
We will prove w' < x.
An exact proof term for the current goal is Hx3 w' Hw'.
Assume Hw: w ∈ Ly'.
Apply ReplE_impred Ly (λw ⇒ x + w) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ Ly.
Assume Hwe: w = x + w'.
rewrite the current goal using Hwe (from left to right).
We will prove x + w' < x + y.
Apply add_SNo_Lt2 x w' y Hx1 (HLRy1 w' Hw') Hy1 to the current goal.
We will prove w' < y.
An exact proof term for the current goal is Hy3 w' Hw'.
rewrite the current goal using add_SNo_eq x Hx1 y Hy1 (from right to left).
We will prove ∀z ∈ Rx' ∪ Ry', x + y < z.
Let z be given.
Apply binunionE' to the current goal.
Assume Hz: z ∈ Rx'.
Apply ReplE_impred Rx (λz ⇒ z + y) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Rx.
Assume Hze: z = z' + y.
rewrite the current goal using Hze (from left to right).
We will prove x + y < z' + y.
Apply add_SNo_Lt1 x y z' Hx1 Hy1 (HLRx2 z' Hz') to the current goal.
We will prove x < z'.
An exact proof term for the current goal is Hx4 z' Hz'.
Assume Hz: z ∈ Ry'.
Apply ReplE_impred Ry (λz ⇒ x + z) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Ry.
Assume Hze: z = x + z'.
rewrite the current goal using Hze (from left to right).
We will prove x + y < x + z'.
Apply add_SNo_Lt2 x y z' Hx1 Hy1 (HLRy2 z' Hz') to the current goal.
We will prove y < z'.
An exact proof term for the current goal is Hy4 z' Hz'.
∎