Let a and b be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume Ha0: Rlt 0 a.
Assume Hb0: Rlt 0 b.
We prove the intermediate claim Hex1: ∃N1 ∈ ω, eps_ N1 < a.
An exact proof term for the current goal is (exists_eps_lt_pos_Euclid a HaR Ha0).
Apply Hex1 to the current goal.
Let N1 be given.
Assume HN1pair.
We prove the intermediate claim HN1o: N1 ∈ ω.
An exact proof term for the current goal is (andEL (N1 ∈ ω) (eps_ N1 < a) HN1pair).
We prove the intermediate claim Heps1lt_a: eps_ N1 < a.
An exact proof term for the current goal is (andER (N1 ∈ ω) (eps_ N1 < a) HN1pair).
We prove the intermediate claim Heps1R: eps_ N1 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N1) (SNo_eps_SNoS_omega N1 HN1o)).
We prove the intermediate claim Heps1Rlt: Rlt (eps_ N1) a.
An exact proof term for the current goal is (RltI (eps_ N1) a Heps1R HaR Heps1lt_a).
We prove the intermediate claim Hex2: ∃N2 ∈ ω, eps_ N2 < b.
An exact proof term for the current goal is (exists_eps_lt_pos_Euclid b HbR Hb0).
Apply Hex2 to the current goal.
Let N2 be given.
Assume HN2pair.
We prove the intermediate claim HN2o: N2 ∈ ω.
An exact proof term for the current goal is (andEL (N2 ∈ ω) (eps_ N2 < b) HN2pair).
We prove the intermediate claim Heps2lt_b: eps_ N2 < b.
An exact proof term for the current goal is (andER (N2 ∈ ω) (eps_ N2 < b) HN2pair).
We prove the intermediate claim Heps2R: eps_ N2 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N2) (SNo_eps_SNoS_omega N2 HN2o)).
We prove the intermediate claim Heps2Rlt: Rlt (eps_ N2) b.
An exact proof term for the current goal is (RltI (eps_ N2) b Heps2R HbR Heps2lt_b).
We prove the intermediate claim Hord1: ordinal N1.
An exact proof term for the current goal is (nat_p_ordinal N1 (omega_nat_p N1 HN1o)).
We prove the intermediate claim Hord2: ordinal N2.
An exact proof term for the current goal is (nat_p_ordinal N2 (omega_nat_p N2 HN2o)).
Apply (ordinal_trichotomy_or_impred N1 N2 Hord1 Hord2 (∃r3 : set, r3 ∈ R ∧ Rlt 0 r3 ∧ Rlt r3 a ∧ Rlt r3 b)) to the current goal.
Assume H12: N1 ∈ N2.
Set N to be the term ordsucc N2.
We prove the intermediate claim HNo: N ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N2 HN2o).
Set r3 to be the term eps_ N.
We prove the intermediate claim Hr3R: r3 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real r3 (SNo_eps_SNoS_omega N HNo)).
We prove the intermediate claim Hr3posS: 0 < r3.
An exact proof term for the current goal is (SNo_eps_pos N HNo).
We prove the intermediate claim Hr3pos: Rlt 0 r3.
An exact proof term for the current goal is (RltI 0 r3 real_0 Hr3R Hr3posS).
We prove the intermediate claim HN2in: N2 ∈ N.
An exact proof term for the current goal is (ordsuccI2 N2).
We prove the intermediate claim HN1in: N1 ∈ N.
An exact proof term for the current goal is (ordsuccI1 N2 N1 H12).
We prove the intermediate claim HepsNlt2: r3 < eps_ N2.
An exact proof term for the current goal is (SNo_eps_decr N HNo N2 HN2in).
We prove the intermediate claim HepsNlt1: r3 < eps_ N1.
An exact proof term for the current goal is (SNo_eps_decr N HNo N1 HN1in).
We prove the intermediate claim HepsNlt2Rlt: Rlt r3 (eps_ N2).
An exact proof term for the current goal is (RltI r3 (eps_ N2) Hr3R Heps2R HepsNlt2).
We prove the intermediate claim HepsNlt1Rlt: Rlt r3 (eps_ N1).
An exact proof term for the current goal is (RltI r3 (eps_ N1) Hr3R Heps1R HepsNlt1).
We use r3 to witness the existential quantifier.
Apply and4I to the current goal.
An exact proof term for the current goal is Hr3R.
An exact proof term for the current goal is Hr3pos.
An exact proof term for the current goal is (Rlt_tra r3 (eps_ N1) a HepsNlt1Rlt Heps1Rlt).
An exact proof term for the current goal is (Rlt_tra r3 (eps_ N2) b HepsNlt2Rlt Heps2Rlt).
Assume Heq: N1 = N2.
Set N to be the term ordsucc N1.
We prove the intermediate claim HNo: N ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N1 HN1o).
Set r3 to be the term eps_ N.
We prove the intermediate claim Hr3R: r3 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real r3 (SNo_eps_SNoS_omega N HNo)).
We prove the intermediate claim Hr3posS: 0 < r3.
An exact proof term for the current goal is (SNo_eps_pos N HNo).
We prove the intermediate claim Hr3pos: Rlt 0 r3.
An exact proof term for the current goal is (RltI 0 r3 real_0 Hr3R Hr3posS).
We prove the intermediate claim HN1in: N1 ∈ N.
An exact proof term for the current goal is (ordsuccI2 N1).
We prove the intermediate claim HepsNlt1: r3 < eps_ N1.
An exact proof term for the current goal is (SNo_eps_decr N HNo N1 HN1in).
We prove the intermediate claim HepsNlt1Rlt: Rlt r3 (eps_ N1).
An exact proof term for the current goal is (RltI r3 (eps_ N1) Hr3R Heps1R HepsNlt1).
We use r3 to witness the existential quantifier.
Apply and4I to the current goal.
An exact proof term for the current goal is Hr3R.
An exact proof term for the current goal is Hr3pos.
An exact proof term for the current goal is (Rlt_tra r3 (eps_ N1) a HepsNlt1Rlt Heps1Rlt).
We prove the intermediate claim Heps1Rltb: Rlt (eps_ N1) b.
We will prove Rlt (eps_ N1) b.
rewrite the current goal using Heq (from left to right) at position 1.
An exact proof term for the current goal is Heps2Rlt.
An exact proof term for the current goal is (Rlt_tra r3 (eps_ N1) b HepsNlt1Rlt Heps1Rltb).
Assume H21: N2 ∈ N1.
Set N to be the term ordsucc N1.
We prove the intermediate claim HNo: N ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N1 HN1o).
Set r3 to be the term eps_ N.
We prove the intermediate claim Hr3R: r3 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real r3 (SNo_eps_SNoS_omega N HNo)).
We prove the intermediate claim Hr3posS: 0 < r3.
An exact proof term for the current goal is (SNo_eps_pos N HNo).
We prove the intermediate claim Hr3pos: Rlt 0 r3.
An exact proof term for the current goal is (RltI 0 r3 real_0 Hr3R Hr3posS).
We prove the intermediate claim HN1in: N1 ∈ N.
An exact proof term for the current goal is (ordsuccI2 N1).
We prove the intermediate claim HN2in: N2 ∈ N.
An exact proof term for the current goal is (ordsuccI1 N1 N2 H21).
We prove the intermediate claim HepsNlt1: r3 < eps_ N1.
An exact proof term for the current goal is (SNo_eps_decr N HNo N1 HN1in).
We prove the intermediate claim HepsNlt2: r3 < eps_ N2.
An exact proof term for the current goal is (SNo_eps_decr N HNo N2 HN2in).
We prove the intermediate claim HepsNlt1Rlt: Rlt r3 (eps_ N1).
An exact proof term for the current goal is (RltI r3 (eps_ N1) Hr3R Heps1R HepsNlt1).
We prove the intermediate claim HepsNlt2Rlt: Rlt r3 (eps_ N2).
An exact proof term for the current goal is (RltI r3 (eps_ N2) Hr3R Heps2R HepsNlt2).
We use r3 to witness the existential quantifier.
Apply and4I to the current goal.
An exact proof term for the current goal is Hr3R.
An exact proof term for the current goal is Hr3pos.
An exact proof term for the current goal is (Rlt_tra r3 (eps_ N1) a HepsNlt1Rlt Heps1Rlt).
An exact proof term for the current goal is (Rlt_tra r3 (eps_ N2) b HepsNlt2Rlt Heps2Rlt).
∎