Let x be given.
Assume Hx1 Hx2 Hx3.
Apply SNoS_E2 (ordsucc ω) ordsucc_omega_ordinal x Hx1 to the current goal.
Assume Hx1a Hx1b Hx1c Hx1d.
Apply dneg to the current goal.
Assume HC: ¬ (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k).
We prove the intermediate claim L1: x ∉ SNoS_ ω.
Assume H1: x ∈ SNoS_ ω.
Apply HC to the current goal.
An exact proof term for the current goal is SNoS_omega_drat_intvl x H1.
We prove the intermediate claim L2: ∀k, nat_p k → ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k.
Apply nat_ind to the current goal.
We will prove ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ 0.
rewrite the current goal using eps_0_1 (from left to right).
We will prove ∃q ∈ SNoS_ ω, q < x ∧ x < q + 1.
We prove the intermediate claim L1a: ∀N, nat_p N → - N < x → x < N → ∃q ∈ SNoS_ ω, q < x ∧ x < q + 1.
Apply nat_ind to the current goal.
rewrite the current goal using minus_SNo_0 (from left to right).
Assume H1: 0 < x.
Assume H2: x < 0.
We will prove False.
Apply SNoLt_irref x to the current goal.
An exact proof term for the current goal is SNoLt_tra x 0 x Hx1c SNo_0 Hx1c H2 H1.
Let N be given.
Assume HN.
Assume IHN: - N < x → x < N → ∃q ∈ SNoS_ ω, q < x ∧ x < q + 1.
Assume H1: - ordsucc N < x.
Assume H2: x < ordsucc N.
We will prove ∃q ∈ SNoS_ ω, q < x ∧ x < q + 1.
We prove the intermediate claim LN1: SNo N.
An exact proof term for the current goal is nat_p_SNo N HN.
We prove the intermediate claim LN2: SNo (- N).
An exact proof term for the current goal is SNo_minus_SNo N LN1.
We prove the intermediate claim LN3: N ∈ SNoS_ ω.
Apply omega_SNoS_omega to the current goal.
An exact proof term for the current goal is nat_p_omega N HN.
Apply SNoLt_trichotomy_or_impred x N Hx1c LN1 to the current goal.
Assume H3: x < N.
Apply SNoLt_trichotomy_or_impred x (- N) Hx1c LN2 to the current goal.
Assume H4: x < - N.
We use (- ordsucc N) to witness the existential quantifier.
Apply andI to the current goal.
We will prove - ordsucc N ∈ SNoS_ ω.
Apply minus_SNo_SNoS_omega to the current goal.
We will prove ordsucc N ∈ SNoS_ ω.
Apply omega_SNoS_omega to the current goal.
Apply omega_ordsucc to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is HN.
Apply andI to the current goal.
We will prove - ordsucc N < x.
An exact proof term for the current goal is H1.
We will prove x < - ordsucc N + 1.
rewrite the current goal using add_SNo_1_ordsucc N (nat_p_omega N HN) (from right to left).
We will prove x < - (N + 1) + 1.
rewrite the current goal using minus_add_SNo_distr N 1 LN1 SNo_1 (from left to right).
We will prove x < (- N + - 1) + 1.
rewrite the current goal using add_SNo_minus_R2' (- N) 1 LN2 SNo_1 (from left to right).
We will prove x < - N.
An exact proof term for the current goal is H4.
Assume H4: x = - N.
We will prove False.
Apply L1 to the current goal.
We will prove x ∈ SNoS_ ω.
rewrite the current goal using H4 (from left to right).
Apply minus_SNo_SNoS_omega to the current goal.
We will prove N ∈ SNoS_ ω.
An exact proof term for the current goal is LN3.
Assume H4: - N < x.
An exact proof term for the current goal is IHN H4 H3.
Assume H3: x = N.
We will prove False.
Apply L1 to the current goal.
We will prove x ∈ SNoS_ ω.
rewrite the current goal using H3 (from left to right).
We will prove N ∈ SNoS_ ω.
An exact proof term for the current goal is LN3.
Assume H3: N < x.
We use N to witness the existential quantifier.
Apply andI to the current goal.
We will prove N ∈ SNoS_ ω.
An exact proof term for the current goal is LN3.
Apply andI to the current goal.
We will prove N < x.
An exact proof term for the current goal is H3.
We will prove x < N + 1.
rewrite the current goal using add_SNo_1_ordsucc N (nat_p_omega N HN) (from left to right).
We will prove x < ordsucc N.
An exact proof term for the current goal is H2.
Apply SNoS_ordsucc_omega_bdd_above x Hx1 Hx3 to the current goal.
Let N be given.
Assume HN.
Apply HN to the current goal.
Assume HN1: N ∈ ω.
Assume HN2: x < N.
Apply SNoS_ordsucc_omega_bdd_below x Hx1 Hx2 to the current goal.
Let N' be given.
Assume HN'.
Apply HN' to the current goal.
Assume HN'1: N' ∈ ω.
Assume HN'2: - N' < x.
Apply SNoLt_trichotomy_or_impred N N' (omega_SNo N HN1) (omega_SNo N' HN'1) to the current goal.
Assume H1: N < N'.
Apply L1a N' (omega_nat_p N' HN'1) HN'2 to the current goal.
We will prove x < N'.
An exact proof term for the current goal is SNoLt_tra x N N' Hx1c (omega_SNo N HN1) (omega_SNo N' HN'1) HN2 H1.
Assume H1: N = N'.
Apply L1a N' (omega_nat_p N' HN'1) HN'2 to the current goal.
We will prove x < N'.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is HN2.
Assume H1: N' < N.
Apply L1a N (omega_nat_p N HN1) to the current goal.
We will prove - N < x.
Apply SNoLt_tra (- N) (- N') x (SNo_minus_SNo N (omega_SNo N HN1)) (SNo_minus_SNo N' (omega_SNo N' HN'1)) Hx1c to the current goal.
We will prove - N < - N'.
Apply minus_SNo_Lt_contra N' N (omega_SNo N' HN'1) (omega_SNo N HN1) to the current goal.
An exact proof term for the current goal is H1.
We will prove - N' < x.
An exact proof term for the current goal is HN'2.
We will prove x < N.
An exact proof term for the current goal is HN2.
Let k be given.
Assume Hk.
Assume IHk.
Apply IHk to the current goal.
Let q be given.
Assume H.
Apply H to the current goal.
Assume Hq1: q ∈ SNoS_ ω.
Assume H.
Apply H to the current goal.
Assume Hq2: q < x.
Assume Hq3: x < q + eps_ k.
Apply SNoS_E2 ω omega_ordinal q Hq1 to the current goal.
Assume Hq1a Hq1b Hq1c Hq1d.
We will prove ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ (ordsucc k).
Apply SNoLt_trichotomy_or_impred x (q + eps_ (ordsucc k)) Hx1c (SNo_add_SNo q (eps_ (ordsucc k)) Hq1c (SNo_eps_ (ordsucc k) (omega_ordsucc k (nat_p_omega k Hk)))) to the current goal.
Assume H1: x < q + eps_ (ordsucc k).
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq1.
Apply andI to the current goal.
An exact proof term for the current goal is Hq2.
An exact proof term for the current goal is H1.
Assume H1: x = q + eps_ (ordsucc k).
We will prove False.
Apply L1 to the current goal.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is add_SNo_SNoS_omega q Hq1 (eps_ (ordsucc k)) (SNo_eps_SNoS_omega (ordsucc k) (omega_ordsucc k (nat_p_omega k Hk))).
Assume H1: q + eps_ (ordsucc k) < x.
We use (q + eps_ (ordsucc k)) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is add_SNo_SNoS_omega q Hq1 (eps_ (ordsucc k)) (SNo_eps_SNoS_omega (ordsucc k) (omega_ordsucc k (nat_p_omega k Hk))).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
We will prove x < (q + eps_ (ordsucc k)) + eps_ (ordsucc k).
rewrite the current goal using add_SNo_assoc q (eps_ (ordsucc k)) (eps_ (ordsucc k)) Hq1c (SNo_eps_ (ordsucc k) (omega_ordsucc k (nat_p_omega k Hk))) (SNo_eps_ (ordsucc k) (omega_ordsucc k (nat_p_omega k Hk))) (from right to left).
We will prove x < q + (eps_ (ordsucc k) + eps_ (ordsucc k)).
rewrite the current goal using eps_ordsucc_half_add k Hk (from left to right).
We will prove x < q + eps_ k.
An exact proof term for the current goal is Hq3.
Apply HC to the current goal.
Let k be given.
Assume Hk.
An exact proof term for the current goal is L2 k (omega_nat_p k Hk).
∎