Let x be given.
Assume Hx.
Let f be given.
Assume Hf1.
Let g be given.
Assume Hg1 Hf2 Hf3 Hf4 Hg3 Hg4.
Set L to be the term {f n|n ∈ ω}.
Set R to be the term {g n|n ∈ ω}.
Assume Hxfg: x = SNoCut L R.
We prove the intermediate
claim Lmx:
SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
We prove the intermediate
claim Lf:
∀n ∈ ω, SNo (f n).
Let n be given.
Assume Hn.
Apply SNoS_E2 ω omega_ordinal (f n) (ap_Pi ω (λ_ ⇒ SNoS_ ω) f n Hf1 Hn) to the current goal.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate
claim Lg:
∀n ∈ ω, SNo (g n).
Let n be given.
Assume Hn.
Apply SNoS_E2 ω omega_ordinal (g n) (ap_Pi ω (λ_ ⇒ SNoS_ ω) g n Hg1 Hn) to the current goal.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate
claim Lfg:
∀n m ∈ ω, f n < g m.
Let n be given.
Assume Hn.
Let m be given.
Assume Hm.
Apply SNoLt_tra (f n) x (g m) (Lf n Hn) Hx (Lg m Hm) to the current goal.
An exact proof term for the current goal is Hf2 n Hn.
An exact proof term for the current goal is Hg3 m Hm.
rewrite the current goal using Hxfg (from right to left).
Assume H1: SNoCutP L R.
Assume H2: SNo x.
rewrite the current goal using Hxfg (from right to left).
rewrite the current goal using Hxfg (from right to left).
rewrite the current goal using Hxfg (from right to left).
rewrite the current goal using Hxfg (from right to left).
Apply SNoCutP_SNoCut_impred L R H1 to the current goal.
Assume _ _ _ _.
Apply ordsuccE ω (SNoLev x) H3 to the current goal.
We will
prove x ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal x (SNoLev x) H8 to the current goal.
We will prove SNo_ (SNoLev x) x.
An exact proof term for the current goal is SNoLev_ x Hx.
Assume H8: SNoLev x = ω.
Apply real_I to the current goal.
We will
prove x ∈ SNoS_ (ordsucc ω).
An exact proof term for the current goal is H4.
We will prove x ≠ ω.
Assume H9: x = ω.
We prove the intermediate
claim Lbd1:
x < g 0.
An exact proof term for the current goal is Hg3 0 (nat_p_omega 0 nat_0).
Apply real_E (g 0) (SNoS_omega_real (g 0) (ap_Pi ω (λ_ ⇒ SNoS_ ω) g 0 Hg1 (nat_p_omega 0 nat_0))) to the current goal.
Assume Hg0a: SNo (g 0).
Assume _ _ _.
Assume _ _.
Apply SNoLt_irref x to the current goal.
Apply SNoLt_tra x (g 0) x Hx Hg0a Hx Lbd1 to the current goal.
rewrite the current goal using H9 (from left to right).
An exact proof term for the current goal is Hg0b.
We prove the intermediate
claim Lbd2:
f 0 < x.
An exact proof term for the current goal is Hf2 0 (nat_p_omega 0 nat_0).
Apply real_E (f 0) (SNoS_omega_real (f 0) (ap_Pi ω (λ_ ⇒ SNoS_ ω) f 0 Hf1 (nat_p_omega 0 nat_0))) to the current goal.
Assume Hf0a: SNo (f 0).
Assume _ _.
Assume _ _ _.
Apply SNoLt_irref x to the current goal.
Apply SNoLt_tra x (f 0) x Hx Hf0a Hx to the current goal.
rewrite the current goal using H9 (from left to right).
An exact proof term for the current goal is Hf0b.
An exact proof term for the current goal is Lbd2.
We will
prove ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x.
Let q be given.
Assume Hq1 Hq2.
We will prove q = x.
Apply SNoS_E2 ω omega_ordinal q Hq1 to the current goal.
Assume Hq1a Hq1b Hq1c Hq1d.
We prove the intermediate
claim Lmq:
SNo (- q).
An exact proof term for the current goal is SNo_minus_SNo q Hq1c.
We prove the intermediate
claim Lxmq:
SNo (x + - q).
An
exact proof term for the current goal is
SNo_add_SNo x (- q) Hx Lmq.
We prove the intermediate
claim Lqmx:
SNo (q + - x).
An
exact proof term for the current goal is
SNo_add_SNo q (- x) Hq1c Lmx.
We prove the intermediate
claim L5:
∀w ∈ L, w < q.
Let w be given.
Assume Hw.
Apply ReplE_impred ω (λn ⇒ f n) w Hw to the current goal.
Let n be given.
Assume Hn.
Assume Hwn: w = f n.
rewrite the current goal using Hwn (from left to right).
Apply SNoLtLe_or (f n) q (Lf n Hn) Hq1c to the current goal.
An exact proof term for the current goal is H9.
Apply real_E (f (ordsucc n)) (SNoS_omega_real (f (ordsucc n)) (ap_Pi ω (λ_ ⇒ SNoS_ ω) f (ordsucc n) Hf1 (omega_ordsucc n Hn))) to the current goal.
Assume _ _ _ _ _.
Assume _.
We prove the intermediate claim L5a: SNo (f (ordsucc n)).
An exact proof term for the current goal is Lf (ordsucc n) (omega_ordsucc n Hn).
We prove the intermediate
claim L5b:
q < f (ordsucc n).
Apply SNoLeLt_tra q (f n) (f (ordsucc n)) Hq1c (Lf n Hn) L5a H9 to the current goal.
We will
prove f n < f (ordsucc n).
Apply Hf4 (ordsucc n) (omega_ordsucc n Hn) to the current goal.
We will
prove n ∈ ordsucc n.
Apply ordsuccI2 to the current goal.
We prove the intermediate
claim L5c:
0 < f (ordsucc n) + - q.
An exact proof term for the current goal is SNoLt_minus_pos q (f (ordsucc n)) Hq1c L5a L5b.
We prove the intermediate
claim L5d:
SNo (f (ordsucc n) + - q).
An
exact proof term for the current goal is
SNo_add_SNo (f (ordsucc n)) (- q) L5a Lmq.
We prove the intermediate
claim L5e:
f (ordsucc n) < x.
An exact proof term for the current goal is Hf2 (ordsucc n) (omega_ordsucc n Hn).
We prove the intermediate
claim L5f:
q < x.
An exact proof term for the current goal is SNoLt_tra q (f (ordsucc n)) x Hq1c L5a Hx L5b L5e.
We prove the intermediate
claim L5g:
0 < x + - q.
An exact proof term for the current goal is SNoLt_minus_pos q x Hq1c Hx L5f.
We prove the intermediate
claim L5h:
abs_SNo (q + - x) = x + - q.
rewrite the current goal using abs_SNo_dist_swap q x Hq1c Hx (from left to right).
An
exact proof term for the current goal is
pos_abs_SNo (x + - q) L5g.
We prove the intermediate claim L5i: q = f (ordsucc n).
Apply Hfn2 q Hq1 to the current goal.
Let k be given.
We will
prove abs_SNo (q + - f (ordsucc n)) < eps_ k.
rewrite the current goal using abs_SNo_dist_swap q (f (ordsucc n)) Hq1c (Lf (ordsucc n) (omega_ordsucc n Hn)) (from left to right).
We will
prove abs_SNo (f (ordsucc n) + - q) < eps_ k.
rewrite the current goal using
pos_abs_SNo (f (ordsucc n) + - q) L5c (from left to right).
We will
prove f (ordsucc n) + - q < eps_ k.
Apply SNoLt_tra (f (ordsucc n) + - q) (x + - q) (eps_ k) L5d Lxmq (SNo_eps_ k Hk) to the current goal.
We will
prove f (ordsucc n) + - q < x + - q.
Apply add_SNo_Lt1 (f (ordsucc n)) (- q) x L5a Lmq Hx to the current goal.
We will
prove f (ordsucc n) < x.
An exact proof term for the current goal is L5e.
We will
prove x + - q < eps_ k.
rewrite the current goal using L5h (from right to left).
We will
prove abs_SNo (q + - x) < eps_ k.
An exact proof term for the current goal is Hq2 k Hk.
Apply SNoLt_irref q to the current goal.
rewrite the current goal using L5i (from left to right) at position 2.
An exact proof term for the current goal is L5b.
We prove the intermediate
claim L6:
∀z ∈ R, q < z.
Let z be given.
Apply ReplE_impred ω (λn ⇒ g n) z Hz to the current goal.
Let m be given.
Assume Hm.
Assume Hzm: z = g m.
rewrite the current goal using Hzm (from left to right).
Apply SNoLtLe_or q (g m) Hq1c (Lg m Hm) to the current goal.
An exact proof term for the current goal is H9.
Apply real_E (g (ordsucc m)) (SNoS_omega_real (g (ordsucc m)) (ap_Pi ω (λ_ ⇒ SNoS_ ω) g (ordsucc m) Hg1 (omega_ordsucc m Hm))) to the current goal.
Assume _ _ _ _ _.
Assume _.
We prove the intermediate claim L6a: SNo (g (ordsucc m)).
An exact proof term for the current goal is Lg (ordsucc m) (omega_ordsucc m Hm).
We prove the intermediate
claim L6b:
g (ordsucc m) < q.
Apply SNoLtLe_tra (g (ordsucc m)) (g m) q L6a (Lg m Hm) Hq1c to the current goal.
We will
prove g (ordsucc m) < g m.
Apply Hg4 (ordsucc m) (omega_ordsucc m Hm) to the current goal.
We will
prove m ∈ ordsucc m.
Apply ordsuccI2 to the current goal.
An exact proof term for the current goal is H9.
We prove the intermediate
claim L6c:
0 < q + - g (ordsucc m).
An exact proof term for the current goal is SNoLt_minus_pos (g (ordsucc m)) q L6a Hq1c L6b.
We prove the intermediate
claim L6d:
SNo (q + - g (ordsucc m)).
An
exact proof term for the current goal is
SNo_add_SNo q (- g (ordsucc m)) Hq1c (SNo_minus_SNo (g (ordsucc m)) L6a).
We prove the intermediate
claim L6e:
x < g (ordsucc m).
An exact proof term for the current goal is Hg3 (ordsucc m) (omega_ordsucc m Hm).
We prove the intermediate
claim L6f:
x < q.
An exact proof term for the current goal is SNoLt_tra x (g (ordsucc m)) q Hx L6a Hq1c L6e L6b.
We prove the intermediate
claim L6g:
0 < q + - x.
An exact proof term for the current goal is SNoLt_minus_pos x q Hx Hq1c L6f.
We prove the intermediate
claim L6h:
abs_SNo (q + - x) = q + - x.
An
exact proof term for the current goal is
pos_abs_SNo (q + - x) L6g.
We prove the intermediate claim L6i: q = g (ordsucc m).
Apply Hgm2 q Hq1 to the current goal.
Let k be given.
We will
prove abs_SNo (q + - g (ordsucc m)) < eps_ k.
rewrite the current goal using
pos_abs_SNo (q + - g (ordsucc m)) L6c (from left to right).
We will
prove q + - g (ordsucc m) < eps_ k.
Apply SNoLt_tra (q + - g (ordsucc m)) (q + - x) (eps_ k) L6d Lqmx (SNo_eps_ k Hk) to the current goal.
We will
prove q + - g (ordsucc m) < q + - x.
Apply add_SNo_Lt2 q (- g (ordsucc m)) (- x) Hq1c (SNo_minus_SNo (g (ordsucc m)) L6a) Lmx to the current goal.
We will
prove - g (ordsucc m) < - x.
Apply minus_SNo_Lt_contra x (g (ordsucc m)) Hx L6a to the current goal.
An exact proof term for the current goal is L6e.
We will
prove q + - x < eps_ k.
rewrite the current goal using L6h (from right to left).
We will
prove abs_SNo (q + - x) < eps_ k.
An exact proof term for the current goal is Hq2 k Hk.
Apply SNoLt_irref q to the current goal.
rewrite the current goal using L6i (from left to right) at position 1.
An exact proof term for the current goal is L6b.
Apply H7 q Hq1c L5 L6 to the current goal.
rewrite the current goal using Hxfg (from right to left).
rewrite the current goal using H8 (from left to right).
We will prove False.
Apply In_irref (SNoLev q) to the current goal.
We will
prove SNoLev q ∈ SNoLev q.
Apply H9 to the current goal.
We will
prove SNoLev q ∈ ω.
An exact proof term for the current goal is Hq1a.