Let eps0 be given.

Assume Heps0R: eps0 ∈ R.

Assume Heps0Pos: Rlt 0 eps0.

We prove the intermediate claim HexN0: ∃N0 ∈ ω, eps_ N0 < eps0.

An exact proof term for the current goal is (exists_eps_lt_pos eps0 Heps0R Heps0Pos).

Apply HexN0 to the current goal.

Let N0 be given.

Assume HN0pair.

We prove the intermediate claim HN0omega: N0 ∈ ω.

An exact proof term for the current goal is (andEL (N0 ∈ ω) (eps_ N0 < eps0) HN0pair).

We prove the intermediate claim HepsN0lt: eps_ N0 < eps0.

An exact proof term for the current goal is (andER (N0 ∈ ω) (eps_ N0 < eps0) HN0pair).

We prove the intermediate claim HN0nat: nat_p N0.

An exact proof term for the current goal is (omega_nat_p N0 HN0omega).

We prove the intermediate claim Hsucc0: ordsucc N0 ∈ ω.

An exact proof term for the current goal is (omega_ordsucc N0 HN0omega).

We prove the intermediate claim Hsucc1: ordsucc (ordsucc N0) ∈ ω.

An exact proof term for the current goal is (omega_ordsucc (ordsucc N0) Hsucc0).

Set eps1 to be the term eps_ (ordsucc (ordsucc N0)).

We prove the intermediate claim Heps1R: eps1 ∈ R.

An exact proof term for the current goal is (SNoS_omega_real eps1 (SNo_eps_SNoS_omega (ordsucc (ordsucc N0)) Hsucc1)).

We prove the intermediate claim Heps1S: SNo eps1.

An exact proof term for the current goal is (real_SNo eps1 Heps1R).

We prove the intermediate claim H0lt_eps1: 0 < eps1.

An exact proof term for the current goal is (SNo_eps_pos (ordsucc (ordsucc N0)) Hsucc1).

We prove the intermediate claim Heps1Pos: Rlt 0 eps1.

An exact proof term for the current goal is (RltI 0 eps1 real_0 Heps1R H0lt_eps1).

We prove the intermediate claim Heps2eq: add_SNo eps1 eps1 = eps_ (ordsucc N0).

An exact proof term for the current goal is (eps_ordsucc_half_add (ordsucc N0) (omega_nat_p (ordsucc N0) Hsucc0)).

We prove the intermediate claim Heps4eq: add_SNo (add_SNo eps1 eps1) (add_SNo eps1 eps1) = eps_ N0.

rewrite the current goal using Heps2eq (from left to right).

An exact proof term for the current goal is (eps_ordsucc_half_add N0 HN0nat).

We prove the intermediate claim Heps2R: add_SNo eps1 eps1 ∈ R.

An exact proof term for the current goal is (real_add_SNo eps1 Heps1R eps1 Heps1R).

We prove the intermediate claim HsumR: add_SNo (add_SNo eps1 eps1) (add_SNo eps1 eps1) ∈ R.

An exact proof term for the current goal is (real_add_SNo (add_SNo eps1 eps1) Heps2R (add_SNo eps1 eps1) Heps2R).

We prove the intermediate claim HsumSlt: add_SNo (add_SNo eps1 eps1) (add_SNo eps1 eps1) < eps0.

rewrite the current goal using Heps4eq (from left to right).

An exact proof term for the current goal is HepsN0lt.

We prove the intermediate claim HsumRlt: Rlt (add_SNo (add_SNo eps1 eps1) (add_SNo eps1 eps1)) eps0.

An exact proof term for the current goal is (RltI (add_SNo (add_SNo eps1 eps1) (add_SNo eps1 eps1)) eps0 HsumR Heps0R HsumSlt).

We use eps1 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Heps1R.

An exact proof term for the current goal is Heps1Pos.

An exact proof term for the current goal is HsumRlt.

∎