Let x be given.
Assume HxR Hxpos Hxn2 Hxne.
Apply real_E x HxR to the current goal.
Assume Hx1: SNo x.
Assume Hx2: SNoLev x ∈ ordsucc ω.
Assume Hx3: x ∈ SNoS_ (ordsucc ω).
Assume Hx4: - ω < x.
Assume Hx5: x < ω.
Assume Hx6: ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x.
Assume Hx7: ∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k.
We prove the intermediate claim L1: ∀m, nat_p m → eps_ m < x → ∃w ∈ SNoL_pos x, x < 2 * w.
Apply nat_ind to the current goal.
We will prove eps_ 0 < x → ∃w ∈ SNoL_pos x, x < 2 * w.
rewrite the current goal using eps_0_1 (from left to right).
Assume H1: 1 < x.
Apply SNoLt_trichotomy_or_impred x 2 Hx1 SNo_2 to the current goal.
Assume H2: x < 2.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 1 ∈ SNoL_pos x.
We will prove 1 ∈ {w ∈ SNoL x|0 < w}.
Apply SepI to the current goal.
We will prove 1 ∈ SNoL x.
Apply SNoL_I x Hx1 1 SNo_1 to the current goal.
We will prove SNoLev 1 ∈ SNoLev x.
rewrite the current goal using ordinal_SNoLev 1 (nat_p_ordinal 1 nat_1) (from left to right).
We will prove 1 ∈ SNoLev x.
Apply ordinal_In_Or_Subq 1 (SNoLev x) (nat_p_ordinal 1 nat_1) (SNoLev_ordinal x Hx1) to the current goal.
Assume H3: 1 ∈ SNoLev x.
An exact proof term for the current goal is H3.
Assume H3: SNoLev x ⊆ 1.
We will prove False.
Apply Hxne 0 (nat_p_omega 0 nat_0) to the current goal.
We will prove x = eps_ 0.
rewrite the current goal using eps_0_1 (from left to right).
An exact proof term for the current goal is pos_low_eq_one x Hx1 Hxpos H3.
We will prove 1 < x.
An exact proof term for the current goal is H1.
We will prove 0 < 1.
An exact proof term for the current goal is SNoLt_0_1.
We will prove x < 2 * 1.
rewrite the current goal using mul_SNo_oneR 2 SNo_2 (from left to right).
An exact proof term for the current goal is H2.
Assume H2: x = 2.
We will prove False.
Apply Hxn2 to the current goal.
An exact proof term for the current goal is H2.
Assume H2: 2 < x.
Apply nonneg_real_nat_interval x HxR (SNoLtLe 0 x Hxpos) to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ ω.
Assume H.
Apply H to the current goal.
Assume Hmx: m ≤ x.
Assume Hxm1: x < ordsucc m.
We prove the intermediate claim Lm: nat_p m.
An exact proof term for the current goal is omega_nat_p m Hm.
Apply nat_inv m Lm to the current goal.
Assume Hm0: m = 0.
We will prove False.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
Apply SNoLt_tra x 1 x Hx1 SNo_1 Hx1 to the current goal.
We will prove x < ordsucc 0.
rewrite the current goal using Hm0 (from right to left).
An exact proof term for the current goal is Hxm1.
We will prove 1 < x.
An exact proof term for the current goal is H1.
Assume H.
Apply H to the current goal.
Let m' be given.
Assume H.
Apply H to the current goal.
Assume Hm': nat_p m'.
Assume Hmm': m = ordsucc m'.
Apply nat_inv m' Hm' to the current goal.
Assume Hm'0: m' = 0.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
Apply SNoLt_tra x 2 x Hx1 SNo_2 Hx1 to the current goal.
We will prove x < ordsucc (ordsucc 0).
rewrite the current goal using Hm'0 (from right to left).
rewrite the current goal using Hmm' (from right to left).
An exact proof term for the current goal is Hxm1.
We will prove 2 < x.
An exact proof term for the current goal is H2.
Assume H.
Apply H to the current goal.
Let m'' be given.
Assume H.
Apply H to the current goal.
Assume Hm'': nat_p m''.
Assume Hm'm'': m' = ordsucc m''.
We prove the intermediate claim L1a: ∃k ∈ ω, 2 ≤ k ∧ k < x ∧ x ≤ ordsucc k.
Apply SNoLeE m x (nat_p_SNo m Lm) Hx1 Hmx to the current goal.
Assume H4: m < x.
We use m to witness the existential quantifier.
Apply andI to the current goal.
We will prove m ∈ ω.
An exact proof term for the current goal is Hm.
Apply and3I to the current goal.
We will prove 2 ≤ m.
Apply SNoLtLe_or m 2 (nat_p_SNo m Lm) SNo_2 to the current goal.
Assume H5: m < 2.
We will prove False.
We prove the intermediate claim L1aa: m ∈ 2.
Apply ordinal_SNoLt_In to the current goal.
An exact proof term for the current goal is nat_p_ordinal m Lm.
An exact proof term for the current goal is nat_p_ordinal 2 nat_2.
An exact proof term for the current goal is H5.
Apply cases_2 m L1aa (λi ⇒ m ≠ i) to the current goal.
rewrite the current goal using Hmm' (from left to right).
An exact proof term for the current goal is neq_ordsucc_0 m'.
rewrite the current goal using Hmm' (from left to right).
rewrite the current goal using Hm'm'' (from left to right).
Assume H6: ordsucc (ordsucc m'') = 1.
An exact proof term for the current goal is neq_ordsucc_0 m'' (ordsucc_inj (ordsucc m'') 0 H6).
Use reflexivity.
Assume H5: 2 ≤ m.
An exact proof term for the current goal is H5.
We will prove m < x.
An exact proof term for the current goal is H4.
We will prove x ≤ ordsucc m.
Apply SNoLtLe to the current goal.
We will prove x < ordsucc m.
An exact proof term for the current goal is Hxm1.
Assume H4: m = x.
Apply nat_inv m'' Hm'' to the current goal.
Assume Hm''0: m'' = 0.
We will prove False.
Apply Hxn2 to the current goal.
We will prove x = 2.
rewrite the current goal using H4 (from right to left).
rewrite the current goal using Hmm' (from left to right).
rewrite the current goal using Hm'm'' (from left to right).
rewrite the current goal using Hm''0 (from left to right).
Use reflexivity.
Assume H.
Apply H to the current goal.
Let m''' be given.
Assume H.
Apply H to the current goal.
Assume Hm''': nat_p m'''.
Assume Hm''m''': m'' = ordsucc m'''.
We will prove ∃k ∈ ω, 2 ≤ k ∧ k < x ∧ x ≤ ordsucc k.
We use m' to witness the existential quantifier.
Apply andI to the current goal.
We will prove m' ∈ ω.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is Hm'.
We will prove 2 ≤ m' ∧ m' < x ∧ x ≤ ordsucc m'.
Apply and3I to the current goal.
We will prove 2 ≤ m'.
rewrite the current goal using Hm'm'' (from left to right).
We will prove 2 ≤ ordsucc m''.
rewrite the current goal using ordinal_ordsucc_SNo_eq m'' (nat_p_ordinal m'' Hm'') (from left to right).
We will prove 2 ≤ 1 + m''.
rewrite the current goal using Hm''m''' (from left to right).
We will prove 2 ≤ 1 + ordsucc m'''.
rewrite the current goal using ordinal_ordsucc_SNo_eq m''' (nat_p_ordinal m''' Hm''') (from left to right).
We will prove 2 ≤ 1 + 1 + m'''.
rewrite the current goal using add_SNo_assoc 1 1 m''' SNo_1 SNo_1 (nat_p_SNo m''' Hm''') (from left to right).
We will prove 2 ≤ (1 + 1) + m'''.
rewrite the current goal using add_SNo_1_1_2 (from left to right).
We will prove 2 ≤ 2 + m'''.
rewrite the current goal using add_SNo_0R 2 SNo_2 (from right to left) at position 1.
We will prove 2 + 0 ≤ 2 + m'''.
Apply add_SNo_Le2 2 0 m''' SNo_2 SNo_0 (nat_p_SNo m''' Hm''') to the current goal.
We will prove 0 ≤ m'''.
Apply ordinal_Subq_SNoLe 0 m''' ordinal_Empty (nat_p_ordinal m''' Hm''') to the current goal.
We will prove 0 ⊆ m'''.
Apply Subq_Empty to the current goal.
We will prove m' < x.
rewrite the current goal using H4 (from right to left).
We will prove m' < m.
Apply ordinal_In_SNoLt to the current goal.
An exact proof term for the current goal is nat_p_ordinal m Lm.
rewrite the current goal using Hmm' (from left to right).
Apply ordsuccI2 to the current goal.
We will prove x ≤ ordsucc m'.
rewrite the current goal using H4 (from right to left).
rewrite the current goal using Hmm' (from left to right).
We will prove ordsucc m' ≤ ordsucc m'.
Apply SNoLe_ref to the current goal.
Apply L1a to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ ω.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume H2k: 2 ≤ k.
Assume Hkx: k < x.
Assume HxSk: x ≤ ordsucc k.
We prove the intermediate claim Lk: nat_p k.
An exact proof term for the current goal is omega_nat_p k Hk.
We prove the intermediate claim LkS: SNo k.
An exact proof term for the current goal is nat_p_SNo k Lk.
We use k to witness the existential quantifier.
Apply andI to the current goal.
We will prove k ∈ SNoL_pos x.
We will prove k ∈ {w ∈ SNoL x|0 < w}.
Apply SepI to the current goal.
We will prove k ∈ SNoL x.
Apply SNoL_I to the current goal.
An exact proof term for the current goal is Hx1.
An exact proof term for the current goal is LkS.
We will prove SNoLev k ∈ SNoLev x.
rewrite the current goal using ordinal_SNoLev k (nat_p_ordinal k Lk) (from left to right).
We will prove k ∈ SNoLev x.
Apply ordinal_trichotomy_or_impred k (SNoLev x) (nat_p_ordinal k Lk) (SNoLev_ordinal x Hx1) to the current goal.
Assume H4: k ∈ SNoLev x.
An exact proof term for the current goal is H4.
Assume H4: k = SNoLev x.
We will prove False.
Apply SNoLt_irref k to the current goal.
Apply SNoLtLe_tra k x k LkS Hx1 LkS Hkx to the current goal.
We will prove x ≤ k.
Apply ordinal_SNoLev_max_2 k (nat_p_ordinal k Lk) x Hx1 to the current goal.
rewrite the current goal using H4 (from right to left).
Apply ordsuccI2 to the current goal.
Assume H4: SNoLev x ∈ k.
We will prove False.
Apply SNoLt_irref k to the current goal.
Apply SNoLt_tra k x k LkS Hx1 LkS Hkx to the current goal.
We will prove x < k.
An exact proof term for the current goal is ordinal_SNoLev_max k (nat_p_ordinal k Lk) x Hx1 H4.
We will prove k < x.
An exact proof term for the current goal is Hkx.
We will prove 0 < k.
Apply SNoLtLe_tra 0 2 k SNo_0 SNo_2 LkS SNoLt_0_2 to the current goal.
We will prove 2 ≤ k.
An exact proof term for the current goal is H2k.
We will prove x < 2 * k.
rewrite the current goal using add_SNo_1_1_2 (from right to left).
rewrite the current goal using mul_SNo_distrR 1 1 k SNo_1 SNo_1 LkS (from left to right).
rewrite the current goal using mul_SNo_oneL k LkS (from left to right).
We will prove x < k + k.
Apply SNoLeLt_tra x (ordsucc k) (k + k) Hx1 (nat_p_SNo (ordsucc k) (nat_ordsucc k Lk)) (SNo_add_SNo k k LkS LkS) HxSk to the current goal.
We will prove ordsucc k < k + k.
rewrite the current goal using ordinal_ordsucc_SNo_eq k (nat_p_ordinal k Lk) (from left to right).
We will prove 1 + k < k + k.
Apply add_SNo_Lt1 1 k k SNo_1 LkS LkS to the current goal.
We will prove 1 < k.
Apply SNoLtLe_tra 1 2 k SNo_1 SNo_2 LkS SNoLt_1_2 to the current goal.
We will prove 2 ≤ k.
An exact proof term for the current goal is H2k.
Let m be given.
Assume Hm.
Assume IHm: eps_ m < x → ∃w ∈ SNoL_pos x, x < 2 * w.
Assume H1: eps_ (ordsucc m) < x.
We prove the intermediate claim Lm: m ∈ ω.
An exact proof term for the current goal is nat_p_omega m Hm.
We prove the intermediate claim Lem: SNo (eps_ m).
An exact proof term for the current goal is SNo_eps_ m Lm.
Apply SNoLt_trichotomy_or_impred x (eps_ m) Hx1 Lem to the current goal.
Assume H2: x < eps_ m.
We prove the intermediate claim LSm: ordsucc m ∈ ω.
An exact proof term for the current goal is omega_ordsucc m Lm.
We prove the intermediate claim LeSm: SNo (eps_ (ordsucc m)).
An exact proof term for the current goal is SNo_eps_ (ordsucc m) LSm.
We use (eps_ (ordsucc m)) to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps_ (ordsucc m) ∈ SNoL_pos x.
We will prove eps_ (ordsucc m) ∈ {w ∈ SNoL x|0 < w}.
Apply SepI to the current goal.
We will prove eps_ (ordsucc m) ∈ SNoL x.
Apply SNoL_I x Hx1 (eps_ (ordsucc m)) LeSm to the current goal.
We will prove SNoLev (eps_ (ordsucc m)) ∈ SNoLev x.
Apply SNoLtE x (eps_ m) Hx1 Lem H2 to the current goal.
Let z be given.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ SNoLev x ∩ SNoLev (eps_ m).
Assume Hz3: SNoEq_ (SNoLev z) z x.
Assume Hz4: SNoEq_ (SNoLev z) z (eps_ m).
Assume Hz5: x < z.
Assume Hz6: z < eps_ m.
Assume Hz7: SNoLev z ∉ x.
Assume Hz8: SNoLev z ∈ eps_ m.
We will prove False.
We prove the intermediate claim Lz0: z = 0.
Apply SNoLev_0_eq_0 z Hz1 to the current goal.
We will prove SNoLev z = 0.
Apply eps_ordinal_In_eq_0 m to the current goal.
We will prove ordinal (SNoLev z).
An exact proof term for the current goal is SNoLev_ordinal z Hz1.
We will prove SNoLev z ∈ eps_ m.
An exact proof term for the current goal is Hz8.
Apply SNoLt_irref x to the current goal.
Apply SNoLt_tra x z x Hx1 Hz1 Hx1 Hz5 to the current goal.
We will prove z < x.
rewrite the current goal using Lz0 (from left to right).
An exact proof term for the current goal is Hxpos.
Assume H3: SNoLev x ∈ SNoLev (eps_ m).
Assume H4: SNoEq_ (SNoLev x) x (eps_ m).
Assume H5: SNoLev x ∈ eps_ m.
We will prove False.
We prove the intermediate claim Lx0: x = 0.
Apply SNoLev_0_eq_0 x Hx1 to the current goal.
We will prove SNoLev x = 0.
Apply eps_ordinal_In_eq_0 m to the current goal.
We will prove ordinal (SNoLev x).
An exact proof term for the current goal is SNoLev_ordinal x Hx1.
We will prove SNoLev x ∈ eps_ m.
An exact proof term for the current goal is H5.
Apply SNoLt_irref x to the current goal.
rewrite the current goal using Lx0 (from left to right) at position 1.
An exact proof term for the current goal is Hxpos.
rewrite the current goal using SNoLev_eps_ m Lm (from left to right).
Assume H3: ordsucc m ∈ SNoLev x.
Assume H4: SNoEq_ (ordsucc m) x (eps_ m).
Assume H5: ordsucc m ∉ x.
Apply SNoLtE (eps_ (ordsucc m)) x LeSm Hx1 H1 to the current goal.
Let z be given.
Assume Hz1: SNo z.
rewrite the current goal using SNoLev_eps_ (ordsucc m) LSm (from left to right).
Assume Hz2: SNoLev z ∈ ordsucc (ordsucc m) ∩ SNoLev x.
Assume Hz3: SNoEq_ (SNoLev z) z (eps_ (ordsucc m)).
Assume Hz4: SNoEq_ (SNoLev z) z x.
Assume Hz5: eps_ (ordsucc m) < z.
Assume Hz6: z < x.
Assume Hz7: SNoLev z ∉ eps_ (ordsucc m).
Assume Hz8: SNoLev z ∈ x.
We will prove False.
Apply ordsuccE (ordsucc m) (SNoLev z) (binintersectE1 (ordsucc (ordsucc m)) (SNoLev x) (SNoLev z) Hz2) to the current goal.
Assume H6: SNoLev z ∈ ordsucc m.
We prove the intermediate claim Lz0: z = 0.
Apply SNoLev_0_eq_0 z Hz1 to the current goal.
We will prove SNoLev z = 0.
Apply eps_ordinal_In_eq_0 m to the current goal.
We will prove ordinal (SNoLev z).
An exact proof term for the current goal is SNoLev_ordinal z Hz1.
We will prove SNoLev z ∈ eps_ m.
Apply H4 (SNoLev z) H6 to the current goal.
Assume H7 _.
Apply H7 to the current goal.
We will prove SNoLev z ∈ x.
An exact proof term for the current goal is Hz8.
Apply SNoLt_irref (eps_ (ordsucc m)) to the current goal.
Apply SNoLt_tra (eps_ (ordsucc m)) z (eps_ (ordsucc m)) LeSm Hz1 LeSm Hz5 to the current goal.
We will prove z < eps_ (ordsucc m).
rewrite the current goal using Lz0 (from left to right).
An exact proof term for the current goal is SNo_eps_pos (ordsucc m) LSm.
Assume H6: SNoLev z = ordsucc m.
Apply H5 to the current goal.
rewrite the current goal using H6 (from right to left).
An exact proof term for the current goal is Hz8.
Assume H6: SNoLev (eps_ (ordsucc m)) ∈ SNoLev x.
Assume H7: SNoEq_ (SNoLev (eps_ (ordsucc m))) (eps_ (ordsucc m)) x.
Assume H8: SNoLev (eps_ (ordsucc m)) ∈ x.
An exact proof term for the current goal is H6.
rewrite the current goal using SNoLev_eps_ (ordsucc m) LSm (from left to right).
Assume H6: SNoLev x ∈ ordsucc (ordsucc m).
Assume H7: SNoEq_ (SNoLev x) (eps_ (ordsucc m)) x.
Assume H8: SNoLev x ∉ eps_ (ordsucc m).
We will prove False.
Apply ordsuccE (ordsucc m) (SNoLev x) H6 to the current goal.
Assume H9: SNoLev x ∈ ordsucc m.
An exact proof term for the current goal is In_no2cycle (SNoLev x) (ordsucc m) H9 H3.
Assume H9: SNoLev x = ordsucc m.
Apply In_irref (SNoLev x) to the current goal.
rewrite the current goal using H9 (from left to right) at position 1.
An exact proof term for the current goal is H3.
We will prove eps_ (ordsucc m) < x.
An exact proof term for the current goal is H1.
We will prove 0 < eps_ (ordsucc m).
An exact proof term for the current goal is SNo_eps_pos (ordsucc m) LSm.
We will prove x < 2 * eps_ (ordsucc m).
rewrite the current goal using add_SNo_1_1_2 (from right to left).
rewrite the current goal using mul_SNo_distrR 1 1 (eps_ (ordsucc m)) SNo_1 SNo_1 LeSm (from left to right).
rewrite the current goal using mul_SNo_oneL (eps_ (ordsucc m)) LeSm (from left to right).
rewrite the current goal using eps_ordsucc_half_add m Hm (from left to right).
An exact proof term for the current goal is H2.
Assume H2: x = eps_ m.
We will prove False.
An exact proof term for the current goal is Hxne m (nat_p_omega m Hm) H2.
Assume H2: eps_ m < x.
An exact proof term for the current goal is IHm H2.
We prove the intermediate claim L2: ∃k ∈ ω, eps_ k < x.
Apply dneg to the current goal.
Assume H1: ¬ ∃k ∈ ω, eps_ k < x.
We prove the intermediate claim Lx0: 0 = x.
Apply Hx6 0 to the current goal.
We will prove 0 ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal 0 0 to the current goal.
We will prove 0 ∈ ω.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_0.
We will prove SNo_ 0 0.
Apply ordinal_SNo_ to the current goal.
An exact proof term for the current goal is ordinal_Empty.
We will prove ∀k ∈ ω, abs_SNo (0 + - x) < eps_ k.
Let k be given.
Assume Hk.
rewrite the current goal using add_SNo_0L (- x) (SNo_minus_SNo x Hx1) (from left to right).
rewrite the current goal using abs_SNo_minus x Hx1 (from left to right).
rewrite the current goal using pos_abs_SNo x Hxpos (from left to right).
We will prove x < eps_ k.
Apply SNoLt_trichotomy_or_impred x (eps_ k) Hx1 (SNo_eps_ k Hk) to the current goal.
Assume H2: x < eps_ k.
An exact proof term for the current goal is H2.
Assume H2: x = eps_ k.
We will prove False.
An exact proof term for the current goal is Hxne k Hk H2.
Assume H2: eps_ k < x.
We will prove False.
Apply H1 to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
An exact proof term for the current goal is H2.
Apply SNoLt_irref x to the current goal.
rewrite the current goal using Lx0 (from right to left) at position 1.
An exact proof term for the current goal is Hxpos.
Apply L2 to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ ω.
Assume H1: eps_ k < x.
An exact proof term for the current goal is L1 k (omega_nat_p k Hk) H1.
∎