Let n be given.
Assume Hn.
Set L to be the term
{0}.
We prove the intermediate
claim Ln:
nat_p n.
An
exact proof term for the current goal is
omega_nat_p n Hn.
We prove the intermediate
claim L1:
SNoCutP L R.
An
exact proof term for the current goal is
eps_SNoCutP n Hn.
We prove the intermediate
claim LRS:
∀z ∈ R, SNo z.
Apply L1 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 k be given.
Assume Hk.
Let w be given.
rewrite the current goal using
SingE 0 w Hw (from left to right).
rewrite the current goal using
SNoLev_0 (from left to right).
An exact proof term for the current goal is H2.
Let i be given.
Assume Hi.
rewrite the current goal using
SNoLev_0 (from left to right).
An
exact proof term for the current goal is
In_0_1.
Let k be given.
Assume Hk.
Let z be given.
Let m be given.
rewrite the current goal using Hm2 (from left to right).
An exact proof term for the current goal is Ln.
An exact proof term for the current goal is Hm1.
Apply L3b to the current goal.
An exact proof term for the current goal is H3.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is L3a.
Let i be given.
Apply nat_inv n Ln to the current goal.
An exact proof term for the current goal is Hn0 H2.
Assume H2.
Apply H2 to the current goal.
Let n' be given.
Assume H2.
Apply H2 to the current goal.
We will
prove eps_ n' ∈ R.
Apply ReplI to the current goal.
rewrite the current goal using Hn'2 (from left to right).
rewrite the current goal using Hn'2 (from right to left).
An exact proof term for the current goal is Hi.
Apply xm (n = 0) to the current goal.
We prove the intermediate
claim L4a:
R = 0.
Let z be given.
Assume Hz.
Let m be given.
rewrite the current goal using H2 (from left to right).
An
exact proof term for the current goal is
EmptyE m Hm1.
rewrite the current goal using L4a (from left to right).
rewrite the current goal using
binunion_idr (from left to right).
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is L2.
rewrite the current goal using L3 H2 (from right to left).
rewrite the current goal using L2 (from left to right).
rewrite the current goal using L3 H2 (from left to right).
Let i be given.
Assume Hi.
An exact proof term for the current goal is Ln.
rewrite the current goal using L4 (from left to right).
We prove the intermediate
claim L5:
SNo (eps_ n).
An
exact proof term for the current goal is
SNo_eps_ n Hn.
We prove the intermediate
claim L6:
∀w ∈ L, w < eps_ n.
Let w be given.
Assume Hw.
rewrite the current goal using
SingE 0 w Hw (from left to right).
An
exact proof term for the current goal is
SNo_eps_pos n Hn.
We prove the intermediate
claim L7:
∀z ∈ R, eps_ n < z.
Let z be given.
Assume Hz.
Let m be given.
rewrite the current goal using Hm2 (from left to right).
An
exact proof term for the current goal is
SNo_eps_decr n Hn m Hm1.
Apply H5 (eps_ n) L5 L6 L7 to the current goal.
Use symmetry.
rewrite the current goal using
SNoLev_eps_ n Hn (from left to right).
We prove the intermediate
claim L8:
eps_ n < SNoCut L R.
An
exact proof term for the current goal is
SNoLev_ (SNoCut L R) H1.
Apply H3 to the current goal.
Apply SingI to the current goal.
Let z be given.
We prove the intermediate
claim L9:
∀w ∈ L, w < z.
Let w be given.
Assume Hw.
rewrite the current goal using
SingE 0 w Hw (from left to right).
An
exact proof term for the current goal is
SNo_eps_pos n Hn.
An exact proof term for the current goal is Hz5.
We prove the intermediate
claim L10:
∀v ∈ R, z < v.
Let v be given.
Assume Hv.
Apply SNoLt_tra z (SNoCut L R) v Hz1 H1 (LRS v Hv) Hz6 to the current goal.
Apply H4 to the current goal.
An exact proof term for the current goal is Hv.
Apply H5 z Hz1 L9 L10 to the current goal.
Apply H9 to the current goal.
rewrite the current goal using
SNoLev_eps_ n Hn (from left to right).
rewrite the current goal using
SNoLev_eps_ n Hn (from left to right).
An exact proof term for the current goal is H9.
An exact proof term for the current goal is H1.
Apply H3 to the current goal.
Apply SingI to the current goal.
An exact proof term for the current goal is H10.
Apply L11 to the current goal.
Let m be given.
Assume H12.
Apply H12 to the current goal.
rewrite the current goal using Hm2 (from right to left) at position 1.
Apply H4 to the current goal.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hm1.
An exact proof term for the current goal is H8.
An exact proof term for the current goal is H7.
∎