Let x and y be given.
Assume Hx Hy.
Apply Hy to the current goal.
Assume H.
Apply H to the current goal.
Assume Hy1: y ∈ SNoL x.
Assume Hy2: SNo y.
Assume Hy3: ∀w ∈ SNoL x, SNo w → w ≤ y.
Apply SNoL_E x Hx y Hy1 to the current goal.
Assume Hy1a.
Assume Hy1b: SNoLev y ∈ SNoLev x.
Assume Hy1c: y < x.
Apply SNoLev_ind to the current goal.
Let z be given.
Assume Hz: SNo z.
Assume IH: ∀w ∈ SNoS_ (SNoLev z), x < w → y + w < x + x → ∃u ∈ SNoR w, y + u = x + x.
Assume H1: x < z.
Assume H2: y + z < x + x.
We will prove ∃w ∈ SNoR z, y + w = x + x.
We prove the intermediate claim Lxx: SNo (x + x).
An exact proof term for the current goal is SNo_add_SNo x x Hx Hx.
We prove the intermediate claim Lyz: SNo (y + z).
An exact proof term for the current goal is SNo_add_SNo y z Hy2 Hz.
We prove the intermediate claim L1: ∀w ∈ SNoR y, w + z ≤ x + x → False.
Let w be given.
Assume Hw.
Assume H3: w + z ≤ x + x.
Apply SNoR_E y Hy2 w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y.
Assume Hw3: y < w.
Apply SNoLt_irref (x + x) to the current goal.
We will prove x + x < x + x.
Apply SNoLtLe_tra (x + x) (w + z) (x + x) Lxx (SNo_add_SNo w z Hw1 Hz) Lxx to the current goal.
We will prove x + x < w + z.
Apply add_SNo_Lt3b x x w z Hx Hx Hw1 Hz to the current goal.
We will prove x ≤ w.
Apply SNoLtLe_or w x Hw1 Hx to the current goal.
Assume H4: w < x.
We prove the intermediate claim L1a: w ∈ SNoL x.
Apply SNoL_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 ordinal_TransSet (SNoLev x) (SNoLev_ordinal x Hx) (SNoLev y) Hy1b (SNoLev w) Hw2.
We will prove w < x.
An exact proof term for the current goal is H4.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
Apply SNoLtLe_tra y w y Hy2 Hw1 Hy2 Hw3 to the current goal.
We will prove w ≤ y.
An exact proof term for the current goal is Hy3 w L1a Hw1.
Assume H4: x ≤ w.
An exact proof term for the current goal is H4.
We will prove x < z.
An exact proof term for the current goal is H1.
We will prove w + z ≤ x + x.
An exact proof term for the current goal is H3.
We prove the intermediate claim L2: ∀w ∈ SNoL x, y + z ≤ w + x → False.
Let w be given.
Assume Hw.
Assume H3: y + z ≤ w + x.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x.
Assume Hw3: w < x.
Apply SNoLt_irref (w + x) to the current goal.
We will prove w + x < w + x.
Apply SNoLtLe_tra (w + x) (w + z) (w + x) (SNo_add_SNo w x Hw1 Hx) (SNo_add_SNo w z Hw1 Hz) (SNo_add_SNo w x Hw1 Hx) to the current goal.
We will prove w + x < w + z.
Apply add_SNo_Lt2 w x z Hw1 Hx Hz to the current goal.
We will prove x < z.
An exact proof term for the current goal is H1.
We will prove w + z ≤ w + x.
Apply SNoLe_tra (w + z) (y + z) (w + x) (SNo_add_SNo w z Hw1 Hz) Lyz (SNo_add_SNo w x Hw1 Hx) to the current goal.
We will prove w + z ≤ y + z.
Apply add_SNo_Le1 w z y Hw1 Hz Hy2 to the current goal.
We will prove w ≤ y.
An exact proof term for the current goal is Hy3 w Hw Hw1.
We will prove y + z ≤ w + x.
An exact proof term for the current goal is H3.
We prove the intermediate claim L3: ∀w ∈ SNoR z, y + w < x + x → ∃w ∈ SNoR z, y + w = x + x.
Let w be given.
Assume Hw: w ∈ SNoR z.
Assume H4: y + w < x + x.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2.
Assume Hw3: z < w.
We prove the intermediate claim LIH: ∃u ∈ SNoR w, y + u = x + x.
Apply IH w (SNoR_SNoS_ z w Hw) to the current goal.
We will prove x < w.
An exact proof term for the current goal is SNoLt_tra x z w Hx Hz Hw1 H1 Hw3.
We will prove y + w < x + x.
An exact proof term for the current goal is H4.
Apply LIH to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu1: u ∈ SNoR w.
Assume Hu2: y + u = x + x.
Apply SNoR_E w Hw1 u Hu1 to the current goal.
Assume Hu1a Hu1b Hu1c.
We use u to witness the existential quantifier.
Apply andI to the current goal.
We will prove u ∈ SNoR z.
Apply SNoR_I z Hz u Hu1a to the current goal.
We will prove SNoLev u ∈ SNoLev z.
An exact proof term for the current goal is ordinal_TransSet (SNoLev z) (SNoLev_ordinal z Hz) (SNoLev w) Hw2 (SNoLev u) Hu1b.
We will prove z < u.
An exact proof term for the current goal is SNoLt_tra z w u Hz Hw1 Hu1a Hw3 Hu1c.
An exact proof term for the current goal is Hu2.
Apply SNoLt_SNoL_or_SNoR_impred (y + z) (x + x) Lyz Lxx H2 to the current goal.
Let u be given.
Assume Hu1: u ∈ SNoL (x + x).
Assume Hu2: u ∈ SNoR (y + z).
Apply SNoL_E (x + x) Lxx u Hu1 to the current goal.
Assume Hu1a: SNo u.
Assume Hu1b.
Assume Hu1c: u < x + x.
Apply add_SNo_SNoR_interpolate y z Hy2 Hz u Hu2 to the current goal.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR y.
Assume H4: w + z ≤ u.
Apply SNoR_E y Hy2 w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2.
Assume Hw3: y < w.
We will prove False.
Apply L1 w Hw to the current goal.
We will prove w + z ≤ x + x.
Apply SNoLtLe to the current goal.
We will prove w + z < x + x.
Apply SNoLeLt_tra (w + z) u (x + x) (SNo_add_SNo w z Hw1 Hz) Hu1a Lxx H4 to the current goal.
We will prove u < x + x.
An exact proof term for the current goal is Hu1c.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR z.
Assume H4: y + w ≤ u.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2.
Assume Hw3: z < w.
Apply L3 w Hw to the current goal.
We will prove y + w < x + x.
Apply SNoLeLt_tra (y + w) u (x + x) (SNo_add_SNo y w Hy2 Hw1) Hu1a Lxx H4 to the current goal.
We will prove u < x + x.
An exact proof term for the current goal is Hu1c.
Assume H3: y + z ∈ SNoL (x + x).
We will prove False.
Apply add_SNo_SNoL_interpolate x x Hx Hx (y + z) H3 to the current goal.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoL x.
Assume H4: y + z ≤ w + x.
An exact proof term for the current goal is L2 w Hw H4.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoL x.
Assume H4: y + z ≤ x + w.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
Apply L2 w Hw to the current goal.
We will prove y + z ≤ w + x.
rewrite the current goal using add_SNo_com w x Hw1 Hx (from left to right).
We will prove y + z ≤ x + w.
An exact proof term for the current goal is H4.
Assume H3: x + x ∈ SNoR (y + z).
Apply add_SNo_SNoR_interpolate y z Hy2 Hz (x + x) H3 to the current goal.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR y.
Assume H4: w + z ≤ x + x.
We will prove False.
An exact proof term for the current goal is L1 w Hw H4.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR z.
Assume H4: y + w ≤ x + x.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev z.
Assume Hw3: z < w.
Apply SNoLtLe_or (y + w) (x + x) (SNo_add_SNo y w Hy2 Hw1) Lxx to the current goal.
Assume H5: y + w < x + x.
We will prove ∃w ∈ SNoR z, y + w = x + x.
Apply L3 w Hw to the current goal.
We will prove y + w < x + x.
An exact proof term for the current goal is H5.
Assume H5: x + x ≤ y + w.
We will prove ∃w ∈ SNoR z, y + w = x + x.
We use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw.
Apply SNoLe_antisym (y + w) (x + x) (SNo_add_SNo y w Hy2 Hw1) Lxx to the current goal.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H5.
∎