Apply nat_complete_ind to the current goal.
Let n be given.
Assume Hn.
Assume IH: ∀m ∈ n, eps_ (ordsucc m) + eps_ (ordsucc m) = eps_ m.
We prove the intermediate claim Ln: n ∈ ω.
An exact proof term for the current goal is nat_p_omega n Hn.
rewrite the current goal using eps_SNoCut n Ln (from left to right).
Set x to be the term eps_ (ordsucc n).
We prove the intermediate claim Lx: SNo x.
An exact proof term for the current goal is SNo_eps_ (ordsucc n) (omega_ordsucc n Ln).
We prove the intermediate claim Lx2: 0 < x.
An exact proof term for the current goal is SNo_eps_pos (ordsucc n) (omega_ordsucc n Ln).
rewrite the current goal using add_SNo_eq x Lx x Lx (from left to right).
We will prove SNoCut ({w + x|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL x}) ({z + x|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR x}) = SNoCut {0} {eps_ m|m ∈ n}.
Apply SNoCut_ext ({w + x|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL x}) ({z + x|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR x}) {0} {eps_ m|m ∈ n} (add_SNo_SNoCutP x x Lx Lx) (eps_SNoCutP n Ln) to the current goal.
We prove the intermediate claim L1: ∀w ∈ SNoL x, w + x < eps_ n ∧ x + w < eps_ n.
Let w be given.
Assume Hw: w ∈ SNoL x.
Apply SNoL_E x Lx w Hw to the current goal.
Assume Hw1: SNo w.
rewrite the current goal using SNoLev_eps_ (ordsucc n) (omega_ordsucc n Ln) (from left to right).
Assume Hw2: SNoLev w ∈ ordsucc (ordsucc n).
Assume Hw3: w < x.
We prove the intermediate claim Lw0: w ≤ 0.
Apply SNoLtLe_or 0 w SNo_0 Hw1 to the current goal.
Assume H1: 0 < w.
We will prove False.
Apply SNoLt_irref w to the current goal.
We will prove w < w.
Apply SNoLt_tra w x w Hw1 Lx Hw1 Hw3 to the current goal.
We will prove x < w.
Apply SNo_pos_eps_Lt (ordsucc n) (nat_ordsucc n Hn) w to the current goal.
We will prove w ∈ SNoS_ (ordsucc (ordsucc n)).
Apply SNoS_I (ordsucc (ordsucc n)) (nat_p_ordinal (ordsucc (ordsucc n)) (nat_ordsucc (ordsucc n) (nat_ordsucc n Hn))) w (SNoLev w) Hw2 to the current goal.
We will prove SNo_ (SNoLev w) w.
An exact proof term for the current goal is SNoLev_ w Hw1.
We will prove 0 < w.
An exact proof term for the current goal is H1.
Assume H1: w ≤ 0.
An exact proof term for the current goal is H1.
We prove the intermediate claim L1a: w + x < eps_ n.
Apply SNoLeLt_tra (w + x) (0 + x) (eps_ n) to the current goal.
An exact proof term for the current goal is SNo_add_SNo w x Hw1 Lx.
An exact proof term for the current goal is SNo_add_SNo 0 x SNo_0 Lx.
An exact proof term for the current goal is SNo_eps_ n Ln.
We will prove w + x ≤ 0 + x.
An exact proof term for the current goal is add_SNo_Le1 w x 0 Hw1 Lx SNo_0 Lw0.
We will prove 0 + x < eps_ n.
rewrite the current goal using add_SNo_0L x Lx (from left to right).
We will prove eps_ (ordsucc n) < eps_ n.
An exact proof term for the current goal is SNo_eps_decr (ordsucc n) (omega_ordsucc n Ln) n (ordsuccI2 n).
Apply andI to the current goal.
An exact proof term for the current goal is L1a.
rewrite the current goal using add_SNo_com x w Lx Hw1 (from left to right).
An exact proof term for the current goal is L1a.
Let w' be given.
Assume Hw': w' ∈ {w + x|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL x}.
We will prove w' < SNoCut {0} {eps_ m|m ∈ n}.
rewrite the current goal using eps_SNoCut n Ln (from right to left).
We will prove w' < eps_ n.
Apply binunionE {w + x|w ∈ SNoL x} {x + w|w ∈ SNoL x} w' Hw' to the current goal.
Assume Hw': w' ∈ {w + x|w ∈ SNoL x}.
Apply ReplE_impred (SNoL x) (λw ⇒ w + x) w' Hw' to the current goal.
Let w be given.
Assume Hw1: w ∈ SNoL x.
Assume Hw2: w' = w + x.
rewrite the current goal using Hw2 (from left to right).
An exact proof term for the current goal is andEL (w + x < eps_ n) (x + w < eps_ n) (L1 w Hw1).
Assume Hw': w' ∈ {x + w|w ∈ SNoL x}.
Apply ReplE_impred (SNoL x) (λw ⇒ x + w) w' Hw' to the current goal.
Let w be given.
Assume Hw1: w ∈ SNoL x.
Assume Hw2: w' = x + w.
rewrite the current goal using Hw2 (from left to right).
An exact proof term for the current goal is andER (w + x < eps_ n) (x + w < eps_ n) (L1 w Hw1).
We prove the intermediate claim L2: ∀z ∈ SNoR x, eps_ n < z + x ∧ eps_ n < x + z.
Let z be given.
Assume Hz: z ∈ SNoR x.
Apply SNoR_E x Lx z Hz to the current goal.
Assume Hz1: SNo z.
rewrite the current goal using SNoLev_eps_ (ordsucc n) (omega_ordsucc n Ln) (from left to right).
Assume Hz2: SNoLev z ∈ ordsucc (ordsucc n).
Assume Hz3: x < z.
We prove the intermediate claim L2a: eps_ n < z + x.
Apply SNoLeLt_tra (eps_ n) z (z + x) (SNo_eps_ n Ln) Hz1 to the current goal.
An exact proof term for the current goal is SNo_add_SNo z x Hz1 Lx.
We will prove eps_ n ≤ z.
Apply SNo_pos_eps_Le n Hn z to the current goal.
We will prove z ∈ SNoS_ (ordsucc (ordsucc n)).
Apply SNoS_I (ordsucc (ordsucc n)) (nat_p_ordinal (ordsucc (ordsucc n)) (nat_ordsucc (ordsucc n) (nat_ordsucc n Hn))) z (SNoLev z) Hz2 to the current goal.
We will prove SNo_ (SNoLev z) z.
An exact proof term for the current goal is SNoLev_ z Hz1.
We will prove 0 < z.
Apply SNoLt_tra 0 x z SNo_0 Lx Hz1 to the current goal.
We will prove 0 < x.
An exact proof term for the current goal is SNo_eps_pos (ordsucc n) (omega_ordsucc n Ln).
We will prove x < z.
An exact proof term for the current goal is Hz3.
We will prove z < z + x.
rewrite the current goal using add_SNo_0R z Hz1 (from right to left) at position 1.
We will prove z + 0 < z + x.
Apply add_SNo_Lt2 z 0 x Hz1 SNo_0 Lx to the current goal.
We will prove 0 < x.
An exact proof term for the current goal is SNo_eps_pos (ordsucc n) (omega_ordsucc n Ln).
Apply andI to the current goal.
An exact proof term for the current goal is L2a.
rewrite the current goal using add_SNo_com x z Lx Hz1 (from left to right).
An exact proof term for the current goal is L2a.
Let z' be given.
Assume Hz': z' ∈ {z + x|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR x}.
We will prove SNoCut {0} {eps_ m|m ∈ n} < z'.
rewrite the current goal using eps_SNoCut n Ln (from right to left).
We will prove eps_ n < z'.
Apply binunionE {z + x|z ∈ SNoR x} {x + z|z ∈ SNoR x} z' Hz' to the current goal.
Assume Hz': z' ∈ {z + x|z ∈ SNoR x}.
Apply ReplE_impred (SNoR x) (λz ⇒ z + x) z' Hz' to the current goal.
Let z be given.
Assume Hz1: z ∈ SNoR x.
Assume Hz2: z' = z + x.
rewrite the current goal using Hz2 (from left to right).
We will prove eps_ n < z + x.
An exact proof term for the current goal is andEL (eps_ n < z + x) (eps_ n < x + z) (L2 z Hz1).
Assume Hz': z' ∈ {x + z|z ∈ SNoR x}.
Apply ReplE_impred (SNoR x) (λz ⇒ x + z) z' Hz' to the current goal.
Let z be given.
Assume Hz1: z ∈ SNoR x.
Assume Hz2: z' = x + z.
rewrite the current goal using Hz2 (from left to right).
We will prove eps_ n < x + z.
An exact proof term for the current goal is andER (eps_ n < z + x) (eps_ n < x + z) (L2 z Hz1).
Let w be given.
Assume Hw: w ∈ {0}.
We will prove w < SNoCut ({w + x|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL x}) ({z + x|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR x}).
rewrite the current goal using SingE 0 w Hw (from left to right).
We will prove 0 < SNoCut ({w + x|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL x}) ({z + x|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR x}).
rewrite the current goal using add_SNo_eq x Lx x Lx (from right to left).
We will prove 0 < x + x.
rewrite the current goal using add_SNo_0L 0 SNo_0 (from right to left).
We will prove 0 + 0 < x + x.
An exact proof term for the current goal is add_SNo_Lt3 0 0 x x SNo_0 SNo_0 Lx Lx Lx2 Lx2.
Let z be given.
Assume Hz: z ∈ {eps_ m|m ∈ n}.
We will prove SNoCut ({w + x|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL x}) ({z + x|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR x}) < z.
rewrite the current goal using add_SNo_eq x Lx x Lx (from right to left).
We will prove x + x < z.
Apply ReplE_impred n eps_ z Hz to the current goal.
Let m be given.
Assume Hm1: m ∈ n.
Assume Hm2: z = eps_ m.
rewrite the current goal using Hm2 (from left to right).
We will prove x + x < eps_ m.
rewrite the current goal using IH m Hm1 (from right to left).
We will prove x + x < eps_ (ordsucc m) + eps_ (ordsucc m).
Set y to be the term eps_ (ordsucc m).
We will prove x + x < y + y.
We prove the intermediate claim Lm: m ∈ ω.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_p_trans n Hn m Hm1.
We prove the intermediate claim Ly: SNo y.
An exact proof term for the current goal is SNo_eps_ (ordsucc m) (omega_ordsucc m Lm).
We prove the intermediate claim Lxy: x < y.
Apply SNo_eps_decr (ordsucc n) (omega_ordsucc n Ln) (ordsucc m) to the current goal.
We will prove ordsucc m ∈ ordsucc n.
Apply ordinal_ordsucc_In to the current goal.
We will prove ordinal n.
An exact proof term for the current goal is nat_p_ordinal n Hn.
An exact proof term for the current goal is Hm1.
An exact proof term for the current goal is add_SNo_Lt3 x x y y Lx Lx Ly Ly Lxy Lxy.
∎