We will prove atleastp rational ω.

Set denom to be the term λq ⇒ Eps_i (λn ⇒ n ∈ ω ∧ ∃m ∈ ω, q = m :/: n) of type set → set.

Set num to be the term λq ⇒ Eps_i (λm ⇒ m ∈ ω ∧ q = m :/: denom q) of type set → set.

We prove the intermediate claim L1: ∀q ∈ rational, 0 ≤ q → ∃n ∈ ω, ∃m ∈ ω, q = m :/: n.

Let q be given.

Assume Hq Hqnn.

Apply SepE real (λq ⇒ ∃m ∈ int, ∃n ∈ ω ∖ {0}, q = m :/: n) q Hq to the current goal.

Assume HqR: q ∈ real.

Assume HqQ.

Apply HqQ to the current goal.

Let m be given.

Assume H.

Apply H to the current goal.

Assume Hm: m ∈ int.

Assume H.

Apply H to the current goal.

Let n be given.

Assume H.

Apply H to the current goal.

Assume Hn: n ∈ ω ∖ {0}.

Assume H1: q = m :/: n.

Apply setminusE ω {0} n Hn to the current goal.

Assume Hno: n ∈ ω.

Assume Hnz: n ∉ {0}.

We prove the intermediate claim LnS: SNo n.

An exact proof term for the current goal is omega_SNo n Hno.

We prove the intermediate claim LqS: SNo q.

An exact proof term for the current goal is real_SNo q HqR.

We prove the intermediate claim Lnpos: 0 < n.

Apply SNoLeE 0 n SNo_0 LnS (omega_nonneg n Hno) to the current goal.

Assume H2: 0 < n.

An exact proof term for the current goal is H2.

Assume H2: 0 = n.

We will prove False.

Apply Hnz to the current goal.

We will prove n ∈ {0}.

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

Apply SingI to the current goal.

We prove the intermediate claim Lrnpos: 0 < recip_SNo n.

An exact proof term for the current goal is recip_SNo_of_pos_is_pos n LnS Lnpos.

Apply int_3_cases m Hm to the current goal.

Let m' be given.

Assume Hm': m' ∈ ω.

Assume H2: m = - ordsucc m'.

We will prove False.

Apply SNoLt_irref 0 to the current goal.

We will prove 0 < 0.

Apply SNoLeLt_tra 0 q 0 SNo_0 LqS SNo_0 Hqnn to the current goal.

We will prove q < 0.

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

We will prove m :/: n < 0.

We will prove m * recip_SNo n < 0.

rewrite the current goal using mul_SNo_zeroL (recip_SNo n) (SNo_recip_SNo n LnS) (from right to left).

We will prove m * recip_SNo n < 0 * recip_SNo n.

Apply pos_mul_SNo_Lt' m 0 (recip_SNo n) (int_SNo m Hm) SNo_0 (SNo_recip_SNo n LnS) Lrnpos to the current goal.

We will prove m < 0.

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

We will prove - ordsucc m' < 0.

Apply minus_SNo_Lt_contra1 0 (ordsucc m') SNo_0 (omega_SNo (ordsucc m') (omega_ordsucc m' Hm')) to the current goal.

We will prove - 0 < ordsucc m'.

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

We will prove 0 < ordsucc m'.

Apply ordinal_In_SNoLt (ordsucc m') (nat_p_ordinal (ordsucc m') (nat_ordsucc m' (omega_nat_p m' Hm'))) 0 to the current goal.

We will prove 0 ∈ ordsucc m'.

An exact proof term for the current goal is nat_0_in_ordsucc m' (omega_nat_p m' Hm').

Assume H2: m = 0.

We will prove ∃n ∈ ω, ∃m ∈ ω, q = m :/: n.

We use n to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hno.

We will prove ∃m ∈ ω, q = m :/: n.

We use m to witness the existential quantifier.

Apply andI to the current goal.

We will prove m ∈ ω.

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

Apply nat_p_omega to the current goal.

An exact proof term for the current goal is nat_0.

We will prove q = m :/: n.

An exact proof term for the current goal is H1.

Let m' be given.

Assume Hm': m' ∈ ω.

Assume H2: m = ordsucc m'.

We will prove ∃n ∈ ω, ∃m ∈ ω, q = m :/: n.

We use n to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hno.

We will prove ∃m ∈ ω, q = m :/: n.

We use m to witness the existential quantifier.

Apply andI to the current goal.

We will prove m ∈ ω.

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

We will prove ordsucc m' ∈ ω.

Apply omega_ordsucc to the current goal.

An exact proof term for the current goal is Hm'.

We will prove q = m :/: n.

An exact proof term for the current goal is H1.

We prove the intermediate claim L2: ∀q ∈ rational, 0 ≤ q → denom q ∈ ω ∧ ∃n ∈ ω, q = n :/: denom q.

Let q be given.

Assume Hq Hqnn.

An exact proof term for the current goal is Eps_i_ex (λn ⇒ n ∈ ω ∧ ∃m ∈ ω, q = m :/: n) (L1 q Hq Hqnn).

We prove the intermediate claim L3: ∀q ∈ rational, 0 ≤ q → num q ∈ ω ∧ q = num q :/: denom q.

Let q be given.

Assume Hq Hqnn.

Apply L2 q Hq Hqnn to the current goal.

Assume H2: denom q ∈ ω.

Assume H3: ∃n ∈ ω, q = n :/: denom q.

An exact proof term for the current goal is Eps_i_ex (λm ⇒ m ∈ ω ∧ q = m :/: denom q) H3.

We prove the intermediate claim Lnum: ∀q ∈ rational, 0 ≤ q → num q ∈ ω.

Let q be given.

Assume Hq Hqnn.

Apply L3 q Hq Hqnn to the current goal.

Assume H _.

An exact proof term for the current goal is H.

We prove the intermediate claim Ldenom: ∀q ∈ rational, 0 ≤ q → denom q ∈ ω.

Let q be given.

Assume Hq Hqnn.

Apply L2 q Hq Hqnn to the current goal.

Assume H _.

An exact proof term for the current goal is H.

Set g to be the term λq ⇒ if 0 ≤ q then nat_pair 0 (nat_pair (num q) (denom q)) else nat_pair 1 (nat_pair (num (- q)) (denom (- q))) of type set → set.

We prove the intermediate claim Lgnneg: ∀q, 0 ≤ q → g q = nat_pair 0 (nat_pair (num q) (denom q)).

Let q be given.

Assume Hqnn.

An exact proof term for the current goal is If_i_1 (0 ≤ q) (nat_pair 0 (nat_pair (num q) (denom q))) (nat_pair 1 (nat_pair (num (- q)) (denom (- q)))) Hqnn.

We prove the intermediate claim Lgneg: ∀q, SNo q → q < 0 → g q = nat_pair 1 (nat_pair (num (- q)) (denom (- q))).

Let q be given.

Assume Hq Hqneg.

Apply If_i_0 (0 ≤ q) (nat_pair 0 (nat_pair (num q) (denom q))) (nat_pair 1 (nat_pair (num (- q)) (denom (- q)))) to the current goal.

We will prove ¬ (0 ≤ q).

Assume H1: 0 ≤ q.

Apply SNoLt_irref q to the current goal.

An exact proof term for the current goal is SNoLtLe_tra q 0 q Hq SNo_0 Hq Hqneg H1.

We prove the intermediate claim L_nat_pair_3: ∀k m n ∈ ω, nat_pair k (nat_pair m n) ∈ ω.

Let k be given.

Assume Hk.

Let m be given.

Assume Hm.

Let n be given.

Assume Hn.

An exact proof term for the current goal is nat_pair_In_omega k Hk (nat_pair m n) (nat_pair_In_omega m Hm n Hn).

We prove the intermediate claim L_nat_pair_3_inj: ∀k m n k' m' n' ∈ ω, nat_pair k (nat_pair m n) = nat_pair k' (nat_pair m' n') → ∀p : prop, (k = k' → m = m' → n = n' → p) → p.

Let k be given.

Assume Hk.

Let m be given.

Assume Hm.

Let n be given.

Assume Hn.

Let k' be given.

Assume Hk'.

Let m' be given.

Assume Hm'.

Let n' be given.

Assume Hn'.

Assume H1.

Let p be given.

Assume Hp.

We prove the intermediate claim Lmnm'n': nat_pair m n = nat_pair m' n'.

An exact proof term for the current goal is nat_pair_1 k Hk (nat_pair m n) (nat_pair_In_omega m Hm n Hn) k' Hk' (nat_pair m' n') (nat_pair_In_omega m' Hm' n' Hn') H1.

Apply Hp to the current goal.

An exact proof term for the current goal is nat_pair_0 k Hk (nat_pair m n) (nat_pair_In_omega m Hm n Hn) k' Hk' (nat_pair m' n') (nat_pair_In_omega m' Hm' n' Hn') H1.

An exact proof term for the current goal is nat_pair_0 m Hm n Hn m' Hm' n' Hn' Lmnm'n'.

An exact proof term for the current goal is nat_pair_1 m Hm n Hn m' Hm' n' Hn' Lmnm'n'.

We will prove ∃g : set → set, inj rational ω g.

We use g to witness the existential quantifier.

We will prove inj rational ω g.

Apply injI to the current goal.

Let q be given.

Assume Hq: q ∈ rational.

We prove the intermediate claim LqS: SNo q.

An exact proof term for the current goal is real_SNo q (Subq_rational_real q Hq).

We will prove g q ∈ ω.

Apply SNoLtLe_or q 0 LqS SNo_0 to the current goal.

Assume H1: q < 0.

We prove the intermediate claim LmqQ: - q ∈ rational.

An exact proof term for the current goal is rational_minus_SNo q Hq.

We prove the intermediate claim Lmqnn: 0 ≤ - q.

Apply SNoLtLe to the current goal.

We will prove 0 < - q.

Apply minus_SNo_Lt_contra2 q 0 LqS SNo_0 to the current goal.

We will prove q < - 0.

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

An exact proof term for the current goal is H1.

We will prove g q ∈ ω.

An exact proof term for the current goal is Lgneg q LqS H1 (λ_ u ⇒ u ∈ ω) (L_nat_pair_3 1 (nat_p_omega 1 nat_1) (num (- q)) (Lnum (- q) LmqQ Lmqnn) (denom (- q)) (Ldenom (- q) LmqQ Lmqnn)).

Assume H1: 0 ≤ q.

We will prove g q ∈ ω.

An exact proof term for the current goal is Lgnneg q H1 (λ_ u ⇒ u ∈ ω) (L_nat_pair_3 0 (nat_p_omega 0 nat_0) (num q) (Lnum q Hq H1) (denom q) (Ldenom q Hq H1)).

Let q be given.

Assume Hq: q ∈ rational.

Let q' be given.

Assume Hq': q' ∈ rational.

We prove the intermediate claim LqS: SNo q.

An exact proof term for the current goal is real_SNo q (Subq_rational_real q Hq).

We prove the intermediate claim Lq'S: SNo q'.

An exact proof term for the current goal is real_SNo q' (Subq_rational_real q' Hq').

Assume H1: g q = g q'.

We will prove q = q'.

Apply SNoLtLe_or q 0 LqS SNo_0 to the current goal.

Assume H2: q < 0.

We prove the intermediate claim LmqQ: - q ∈ rational.

An exact proof term for the current goal is rational_minus_SNo q Hq.

We prove the intermediate claim Lmqnn: 0 ≤ - q.

Apply SNoLtLe to the current goal.

We will prove 0 < - q.

Apply minus_SNo_Lt_contra2 q 0 LqS SNo_0 to the current goal.

We will prove q < - 0.

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

An exact proof term for the current goal is H2.

Apply SNoLtLe_or q' 0 Lq'S SNo_0 to the current goal.

Assume H3: q' < 0.

We prove the intermediate claim Lmq'Q: - q' ∈ rational.

An exact proof term for the current goal is rational_minus_SNo q' Hq'.

We prove the intermediate claim Lmq'nn: 0 ≤ - q'.

Apply SNoLtLe to the current goal.

We will prove 0 < - q'.

Apply minus_SNo_Lt_contra2 q' 0 Lq'S SNo_0 to the current goal.

We will prove q' < - 0.

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

An exact proof term for the current goal is H3.

We prove the intermediate claim L4a: nat_pair 1 (nat_pair (num (- q)) (denom (- q))) = nat_pair 1 (nat_pair (num (- q')) (denom (- q'))).

Use transitivity with g q, and g q'.

Use symmetry.

An exact proof term for the current goal is Lgneg q LqS H2.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is Lgneg q' Lq'S H3.

Apply L_nat_pair_3_inj 1 (nat_p_omega 1 nat_1) (num (- q)) (Lnum (- q) LmqQ Lmqnn) (denom (- q)) (Ldenom (- q) LmqQ Lmqnn) 1 (nat_p_omega 1 nat_1) (num (- q')) (Lnum (- q') Lmq'Q Lmq'nn) (denom (- q')) (Ldenom (- q') Lmq'Q Lmq'nn) L4a to the current goal.

Assume _.

Assume Hnmqq': num (- q) = num (- q').

Assume Hdmqq': denom (- q) = denom (- q').

We will prove q = q'.

rewrite the current goal using minus_SNo_invol q LqS (from right to left).

rewrite the current goal using minus_SNo_invol q' Lq'S (from right to left).

We will prove - - q = - - q'.

Use f_equal.

We will prove - q = - q'.

Apply L3 (- q) LmqQ Lmqnn to the current goal.

Assume _.

Assume Hmqnd: - q = num (- q) :/: denom (- q).

Apply L3 (- q') Lmq'Q Lmq'nn to the current goal.

Assume _.

Assume Hmq'nd: - q' = num (- q') :/: denom (- q').

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

rewrite the current goal using Hmq'nd (from left to right).

Use f_equal.

An exact proof term for the current goal is Hnmqq'.

An exact proof term for the current goal is Hdmqq'.

Assume H3: 0 ≤ q'.

We will prove False.

We prove the intermediate claim L4b: nat_pair 1 (nat_pair (num (- q)) (denom (- q))) = nat_pair 0 (nat_pair (num q') (denom q')).

Use transitivity with g q, and g q'.

Use symmetry.

An exact proof term for the current goal is Lgneg q LqS H2.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is Lgnneg q' H3.

Apply L_nat_pair_3_inj 1 (nat_p_omega 1 nat_1) (num (- q)) (Lnum (- q) LmqQ Lmqnn) (denom (- q)) (Ldenom (- q) LmqQ Lmqnn) 0 (nat_p_omega 0 nat_0) (num q') (Lnum q' Hq' H3) (denom q') (Ldenom q' Hq' H3) L4b to the current goal.

Assume H4: 1 = 0.

We will prove False.

Apply neq_1_0 to the current goal.

An exact proof term for the current goal is H4.

Assume H2: 0 ≤ q.

Apply SNoLtLe_or q' 0 Lq'S SNo_0 to the current goal.

Assume H3: q' < 0.

We will prove False.

We prove the intermediate claim Lmq'Q: - q' ∈ rational.

An exact proof term for the current goal is rational_minus_SNo q' Hq'.

We prove the intermediate claim Lmq'nn: 0 ≤ - q'.

Apply SNoLtLe to the current goal.

We will prove 0 < - q'.

Apply minus_SNo_Lt_contra2 q' 0 Lq'S SNo_0 to the current goal.

We will prove q' < - 0.

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

An exact proof term for the current goal is H3.

We prove the intermediate claim L4c: nat_pair 0 (nat_pair (num q) (denom q)) = nat_pair 1 (nat_pair (num (- q')) (denom (- q'))).

Use transitivity with g q, and g q'.

Use symmetry.

An exact proof term for the current goal is Lgnneg q H2.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is Lgneg q' Lq'S H3.

Apply L_nat_pair_3_inj 0 (nat_p_omega 0 nat_0) (num q) (Lnum q Hq H2) (denom q) (Ldenom q Hq H2) 1 (nat_p_omega 1 nat_1) (num (- q')) (Lnum (- q') Lmq'Q Lmq'nn) (denom (- q')) (Ldenom (- q') Lmq'Q Lmq'nn) L4c to the current goal.

Assume H4: 0 = 1.

We will prove False.

Apply neq_0_1 to the current goal.

An exact proof term for the current goal is H4.

Assume H3: 0 ≤ q'.

We prove the intermediate claim L4d: nat_pair 0 (nat_pair (num q) (denom q)) = nat_pair 0 (nat_pair (num q') (denom q')).

Use transitivity with g q, and g q'.

Use symmetry.

An exact proof term for the current goal is Lgnneg q H2.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is Lgnneg q' H3.

Apply L_nat_pair_3_inj 0 (nat_p_omega 0 nat_0) (num q) (Lnum q Hq H2) (denom q) (Ldenom q Hq H2) 0 (nat_p_omega 0 nat_0) (num q') (Lnum q' Hq' H3) (denom q') (Ldenom q' Hq' H3) L4d to the current goal.

Assume _.

Assume Hnqq': num q = num q'.

Assume Hdqq': denom q = denom q'.

We will prove q = q'.

Apply L3 q Hq H2 to the current goal.

Assume _.

Assume Hqnd: q = num q :/: denom q.

Apply L3 q' Hq' H3 to the current goal.

Assume _.

Assume Hq'nd: q' = num q' :/: denom q'.

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

rewrite the current goal using Hq'nd (from left to right).

Use f_equal.

An exact proof term for the current goal is Hnqq'.

An exact proof term for the current goal is Hdqq'.