Let x be given.
Assume H1 H2 H3.
Set f' to be the term nat_primrec (Eps_i (λq ⇒ q ∈ SNoS_ ω ∧ q < x ∧ x < q + eps_ 0)) (λn r ⇒ (Eps_i (λq ⇒ q ∈ SNoS_ ω ∧ q < x ∧ x < q + eps_ (ordsucc n) ∧ r < q))) of type set → set.
Set f to be the term λn ∈ ω ⇒ f' n.
We prove the intermediate claim Lf'0: f' 0 = Eps_i (λq ⇒ q ∈ SNoS_ ω ∧ q < x ∧ x < q + eps_ 0).
An exact proof term for the current goal is nat_primrec_0 (Eps_i (λq ⇒ q ∈ SNoS_ ω ∧ q < x ∧ x < q + eps_ 0)) (λn r ⇒ (Eps_i (λq ⇒ q ∈ SNoS_ ω ∧ q < x ∧ x < q + eps_ (ordsucc n) ∧ r < q))).
We prove the intermediate claim Lf'0b: f' 0 ∈ SNoS_ ω ∧ f' 0 < x ∧ x < f' 0 + eps_ 0.
rewrite the current goal using Lf'0 (from left to right).
Apply Eps_i_ex (λq ⇒ q ∈ SNoS_ ω ∧ q < x ∧ x < q + eps_ 0) to the current goal.
We will prove ∃q, q ∈ SNoS_ ω ∧ q < x ∧ x < q + eps_ 0.
Apply H3 0 (nat_p_omega 0 nat_0) to the current goal.
Let q be given.
Assume Hq.
Apply Hq to the current goal.
Assume Hq1 Hq.
Apply Hq to the current goal.
Assume Hq2 Hq3.
We use q to witness the existential quantifier.
Apply and3I to the current goal.
An exact proof term for the current goal is Hq1.
An exact proof term for the current goal is Hq2.
An exact proof term for the current goal is Hq3.
We prove the intermediate claim Lf'S: ∀n, nat_p n → f' (ordsucc n) = Eps_i (λq ⇒ q ∈ SNoS_ ω ∧ q < x ∧ x < q + eps_ (ordsucc n) ∧ f' n < q).
An exact proof term for the current goal is nat_primrec_S (Eps_i (λq ⇒ q ∈ SNoS_ ω ∧ q < x ∧ x < q + eps_ 0)) (λn r ⇒ (Eps_i (λq ⇒ q ∈ SNoS_ ω ∧ q < x ∧ x < q + eps_ (ordsucc n) ∧ r < q))).
We prove the intermediate claim L1: ∀n, nat_p n → f' n ∈ SNoS_ ω ∧ f' n < x ∧ x < f' n + eps_ n ∧ ∀i ∈ n, SNo (f i) → f i < f' n.
Apply nat_ind to the current goal.
We will prove f' 0 ∈ SNoS_ ω ∧ f' 0 < x ∧ x < f' 0 + eps_ 0 ∧ ∀i ∈ 0, SNo (f i) → f i < f' 0.
Apply Lf'0b to the current goal.
Assume H H6.
Apply H to the current goal.
Assume H4 H5.
Apply and4I to the current goal.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is H6.
Let i be given.
Assume Hi.
We will prove False.
An exact proof term for the current goal is EmptyE i Hi.
Let n be given.
Assume Hn.
Assume IHn: f' n ∈ SNoS_ ω ∧ f' n < x ∧ x < f' n + eps_ n ∧ ∀i ∈ n, SNo (f i) → f i < f' n.
We will prove f' (ordsucc n) ∈ SNoS_ ω ∧ f' (ordsucc n) < x ∧ x < f' (ordsucc n) + eps_ (ordsucc n) ∧ ∀i ∈ ordsucc n, SNo (f i) → f i < f' (ordsucc n).
Apply IHn to the current goal.
Assume IHn123 IHn4.
Apply IHn123 to the current goal.
Assume IHn12 IHn3.
Apply IHn12 to the current goal.
Assume IHn1 IHn2.
Apply SNoS_E2 ω omega_ordinal (f' n) IHn1 to the current goal.
Assume _ _.
Assume IHn1c: SNo (f' n).
Assume _.
We prove the intermediate claim L1b: ∃q, q ∈ SNoS_ ω ∧ q < x ∧ x < q + eps_ (ordsucc n) ∧ f' n < q.
Apply H3 (ordsucc n) (nat_p_omega (ordsucc n) (nat_ordsucc n Hn)) to the current goal.
Let q be given.
Assume Hq.
Apply Hq to the current goal.
Assume Hq1 Hq.
Apply Hq to the current goal.
Assume Hq2 Hq3.
Apply SNoS_E2 ω omega_ordinal q Hq1 to the current goal.
Assume Hq1a Hq1b Hq1c Hq1d.
Apply SNoLtLe_or (f' n) q IHn1c Hq1c to the current goal.
Assume H4: f' n < q.
We use q to witness the existential quantifier.
Apply and4I to the current goal.
An exact proof term for the current goal is Hq1.
An exact proof term for the current goal is Hq2.
An exact proof term for the current goal is Hq3.
An exact proof term for the current goal is H4.
Assume H4: q ≤ f' n.
We prove the intermediate claim L1ba: SNo (- f' n).
An exact proof term for the current goal is SNo_minus_SNo (f' n) IHn1c.
We prove the intermediate claim L1bb: SNo (x + - f' n).
An exact proof term for the current goal is SNo_add_SNo x (- f' n) H1 L1ba.
We prove the intermediate claim L1bc: SNo (eps_ (ordsucc n)).
An exact proof term for the current goal is SNo_eps_ (ordsucc n) (omega_ordsucc n (nat_p_omega n Hn)).
Apply xm (∃k ∈ ω, eps_ k ≤ x + - f' n) to the current goal.
Assume H5.
Apply H5 to the current goal.
Let k be given.
Assume H5.
Apply H5 to the current goal.
Assume Hk1: k ∈ ω.
Assume Hk2: eps_ k ≤ x + - f' n.
We use (f' n + eps_ (ordsucc k)) to witness the existential quantifier.
We prove the intermediate claim Lk1: ordsucc k ∈ ω.
An exact proof term for the current goal is omega_ordsucc k Hk1.
We prove the intermediate claim Lk2: SNo (eps_ (ordsucc k)).
An exact proof term for the current goal is SNo_eps_ (ordsucc k) Lk1.
We prove the intermediate claim Lk3: f' n + eps_ (ordsucc k) ∈ SNoS_ ω.
An exact proof term for the current goal is add_SNo_SNoS_omega (f' n) IHn1 (eps_ (ordsucc k)) (SNo_eps_SNoS_omega (ordsucc k) (omega_ordsucc k Hk1)).
Apply SNoS_E2 ω omega_ordinal (f' n + eps_ (ordsucc k)) Lk3 to the current goal.
Assume _ _.
Assume H6: SNo (f' n + eps_ (ordsucc k)).
Assume _.
Apply and4I to the current goal.
An exact proof term for the current goal is Lk3.
We will prove f' n + eps_ (ordsucc k) < x.
Apply SNoLtLe_tra (f' n + eps_ (ordsucc k)) (f' n + eps_ k) x to the current goal.
An exact proof term for the current goal is H6.
An exact proof term for the current goal is SNo_add_SNo (f' n) (eps_ k) IHn1c (SNo_eps_ k Hk1).
An exact proof term for the current goal is H1.
We will prove f' n + eps_ (ordsucc k) < f' n + eps_ k.
Apply add_SNo_Lt2 (f' n) (eps_ (ordsucc k)) (eps_ k) IHn1c Lk2 (SNo_eps_ k Hk1) to the current goal.
We will prove eps_ (ordsucc k) < eps_ k.
Apply SNo_eps_decr to the current goal.
We will prove ordsucc k ∈ ω.
An exact proof term for the current goal is Lk1.
We will prove k ∈ ordsucc k.
Apply ordsuccI2 to the current goal.
We will prove f' n + eps_ k ≤ x.
Apply add_SNo_minus_L2' (f' n) x IHn1c H1 (λu v ⇒ f' n + eps_ k ≤ u) to the current goal.
We will prove f' n + eps_ k ≤ f' n + (- f' n + x).
rewrite the current goal using add_SNo_com (- f' n) x L1ba H1 (from left to right).
We will prove f' n + eps_ k ≤ f' n + (x + - f' n).
An exact proof term for the current goal is add_SNo_Le2 (f' n) (eps_ k) (x + - f' n) IHn1c (SNo_eps_ k Hk1) L1bb Hk2.
We will prove x < (f' n + eps_ (ordsucc k)) + eps_ (ordsucc n).
rewrite the current goal using add_SNo_com_3b_1_2 (f' n) (eps_ (ordsucc k)) (eps_ (ordsucc n)) IHn1c Lk2 L1bc (from left to right).
We will prove x < (f' n + eps_ (ordsucc n)) + eps_ (ordsucc k).
Apply add_SNo_eps_Lt' x (f' n + eps_ (ordsucc n)) H1 (SNo_add_SNo (f' n) (eps_ (ordsucc n)) IHn1c L1bc) (ordsucc k) Lk1 to the current goal.
We will prove x < f' n + eps_ (ordsucc n).
Apply SNoLtLe_tra x (q + (eps_ (ordsucc n))) to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is SNo_add_SNo q (eps_ (ordsucc n)) Hq1c L1bc.
An exact proof term for the current goal is SNo_add_SNo (f' n) (eps_ (ordsucc n)) IHn1c L1bc.
We will prove x < q + eps_ (ordsucc n).
An exact proof term for the current goal is Hq3.
We will prove q + eps_ (ordsucc n) ≤ f' n + eps_ (ordsucc n).
An exact proof term for the current goal is add_SNo_Le1 q (eps_ (ordsucc n)) (f' n) Hq1c L1bc IHn1c H4.
We will prove f' n < f' n + eps_ (ordsucc k).
An exact proof term for the current goal is add_SNo_eps_Lt (f' n) IHn1c (ordsucc k) (omega_ordsucc k Hk1).
Assume H5: ¬ (∃k ∈ ω, eps_ k ≤ x + - f' n).
We will prove False.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
We prove the intermediate claim L1bd: 0 < x + - f' n.
Apply add_SNo_Lt1_cancel 0 (f' n) (x + - f' n) SNo_0 IHn1c L1bb to the current goal.
We will prove 0 + f' n < (x + - f' n) + f' n.
rewrite the current goal using add_SNo_0L (f' n) IHn1c (from left to right).
rewrite the current goal using add_SNo_minus_R2' x (f' n) H1 IHn1c (from left to right).
We will prove f' n < x.
An exact proof term for the current goal is IHn2.
We prove the intermediate claim L1be: f' n = x.
Apply H2 (f' n) IHn1 to the current goal.
Let k be given.
Assume Hk.
We will prove abs_SNo (f' n + - x) < eps_ k.
Apply SNoLtLe_or (x + - f' n) (eps_ k) L1bb (SNo_eps_ k Hk) to the current goal.
Assume H6: x + - f' n < eps_ k.
We will prove abs_SNo (f' n + - x) < eps_ k.
rewrite the current goal using abs_SNo_dist_swap (f' n) x IHn1c H1 (from left to right).
We will prove abs_SNo (x + - f' n) < eps_ k.
rewrite the current goal using pos_abs_SNo (x + - f' n) L1bd (from left to right).
An exact proof term for the current goal is H6.
Assume H6: eps_ k ≤ x + - f' n.
Apply H5 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 H6.
rewrite the current goal using L1be (from right to left) at position 1.
An exact proof term for the current goal is IHn2.
We prove the intermediate claim L1c: f' (ordsucc n) ∈ SNoS_ ω ∧ f' (ordsucc n) < x ∧ x < f' (ordsucc n) + eps_ (ordsucc n) ∧ f' n < f' (ordsucc n).
rewrite the current goal using Lf'S n Hn (from left to right).
An exact proof term for the current goal is Eps_i_ex (λq ⇒ q ∈ SNoS_ ω ∧ q < x ∧ x < q + eps_ (ordsucc n) ∧ f' n < q) L1b.
Apply L1c to the current goal.
Assume H H7.
Apply H to the current goal.
Assume H H6.
Apply H to the current goal.
Assume H4 H5.
Apply and4I to the current goal.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is H6.
Let i be given.
Assume Hi: i ∈ ordsucc n.
Assume Hfi: SNo (f i).
Apply ordsuccE n i Hi to the current goal.
Assume H8: i ∈ n.
We will prove f i < f' (ordsucc n).
Apply SNoLt_tra (f i) (f' n) (f' (ordsucc n)) to the current goal.
We will prove SNo (f i).
An exact proof term for the current goal is Hfi.
An exact proof term for the current goal is IHn1c.
Apply SNoS_E2 ω omega_ordinal (f' (ordsucc n)) H4 to the current goal.
Assume _ _ H9 _.
An exact proof term for the current goal is H9.
Apply IHn to the current goal.
Assume _.
Assume IHn4: ∀i ∈ n, SNo (f i) → f i < f' n.
An exact proof term for the current goal is IHn4 i H8 Hfi.
An exact proof term for the current goal is H7.
Assume H8: i = n.
rewrite the current goal using H8 (from left to right).
We will prove f n < f' (ordsucc n).
rewrite the current goal using beta ω f' n (nat_p_omega n Hn) (from left to right).
An exact proof term for the current goal is H7.
We prove the intermediate claim L2: ∀n ∈ ω, f' n ∈ SNoS_ ω ∧ f n < x ∧ x < f n + eps_ n ∧ ∀i ∈ n, SNo (f i) → f i < f n.
Let n be given.
Assume Hn.
An exact proof term for the current goal is beta ω f' n Hn (λu v ⇒ f' n ∈ SNoS_ ω ∧ v < x ∧ x < v + eps_ n ∧ ∀i ∈ n, SNo (f i) → f i < v) (L1 n (omega_nat_p n Hn)).
We use f to witness the existential quantifier.
Apply andI to the current goal.
We will prove (λn ∈ ω ⇒ f' n) ∈ ∏n ∈ ω, SNoS_ ω.
Apply lam_Pi to the current goal.
Let n be given.
Assume Hn.
Apply L2 n Hn to the current goal.
Assume H _.
Apply H to the current goal.
Assume H _.
Apply H to the current goal.
Assume H _.
An exact proof term for the current goal is H.
Let n be given.
Assume Hn.
Apply L2 n Hn to the current goal.
Assume H H7.
Apply H to the current goal.
Assume H H6.
Apply H to the current goal.
Assume H4 H5.
Apply and3I to the current goal.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is H6.
Let i be given.
Assume Hi: i ∈ n.
Apply H7 i Hi to the current goal.
We will prove SNo (f i).
We prove the intermediate claim Li: i ∈ ω.
An exact proof term for the current goal is nat_p_omega i (nat_p_trans n (omega_nat_p n Hn) i Hi).
rewrite the current goal using beta ω f' i Li (from left to right).
We will prove SNo (f' i).
Apply L2 i Li to the current goal.
Assume H _.
Apply H to the current goal.
Assume H _.
Apply H to the current goal.
Assume H8: f' i ∈ SNoS_ ω.
Assume _.
Apply SNoS_E2 ω omega_ordinal (f' i) H8 to the current goal.
Assume _ _ H9 _.
We will prove SNo (f' i).
An exact proof term for the current goal is H9.
∎