Let A be given.
Assume HA: A ⊆ R.
Assume Hcomp: compact_space A (subspace_topology R R_standard_topology A).
We will prove closed_in R R_standard_topology A ∧ bounded_subset_of_reals A.
Apply andI to the current goal.
An exact proof term for the current goal is (compact_subspace_in_Hausdorff_closed R R_standard_topology A R_standard_topology_Hausdorff HA Hcomp).
Apply (xm (A = Empty)) to the current goal.
Assume HA0: A = Empty.
We will prove ∃M : set, M ∈ R ∧ ∀x : set, x ∈ A → ¬ (Rlt M (Abs x)).
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is real_0.
Let x be given.
Assume HxA: x ∈ A.
We will prove ¬ (Rlt 0 (Abs x)).
Assume H.
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HA0 (from right to left).
An exact proof term for the current goal is HxA.
An exact proof term for the current goal is (EmptyE x HxE).
Assume HAne: ¬ (A = Empty).
We will prove ∃M : set, M ∈ R ∧ ∀x : set, x ∈ A → ¬ (Rlt M (Abs x)).
We prove the intermediate claim HTtop: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim Hiff: compact_space A (subspace_topology R R_standard_topology A) ↔ ∀Fam : set, (Fam ⊆ R_standard_topology ∧ A ⊆ ⋃ Fam) → has_finite_subcover A R_standard_topology Fam.
An exact proof term for the current goal is (compact_subspace_via_ambient_covers R R_standard_topology A HTtop HA).
We prove the intermediate claim Hcovprop: ∀Fam : set, (Fam ⊆ R_standard_topology ∧ A ⊆ ⋃ Fam) → has_finite_subcover A R_standard_topology Fam.
An exact proof term for the current goal is (iffEL (compact_space A (subspace_topology R R_standard_topology A)) (∀Fam : set, (Fam ⊆ R_standard_topology ∧ A ⊆ ⋃ Fam) → has_finite_subcover A R_standard_topology Fam) Hiff Hcomp).
Set f to be the term λn : set ⇒ open_interval (minus_SNo (ordsucc n)) (ordsucc n).
Set Fam0 to be the term {f n|n ∈ ω}.
We prove the intermediate claim HFam0sub: Fam0 ⊆ R_standard_topology.
Let U be given.
Assume HU: U ∈ Fam0.
Apply (ReplE_impred ω (λn0 : set ⇒ f n0) U HU (U ∈ R_standard_topology)) to the current goal.
Let n0 be given.
Assume Hn0: n0 ∈ ω.
Assume Heq: U = f n0.
rewrite the current goal using Heq (from left to right).
We will prove f n0 ∈ R_standard_topology.
We prove the intermediate claim Hbasis: basis_on R R_standard_basis.
An exact proof term for the current goal is R_standard_basis_is_basis_local.
We prove the intermediate claim Hn0s: ordsucc n0 ∈ R.
An exact proof term for the current goal is (ordsucc_in_R n0 Hn0).
We prove the intermediate claim Hmn0R: minus_SNo (ordsucc n0) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (ordsucc n0) Hn0s).
We prove the intermediate claim HfInBasis: f n0 ∈ R_standard_basis.
Set a to be the term minus_SNo (ordsucc n0).
Set b to be the term ordsucc n0.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is Hmn0R.
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is Hn0s.
We prove the intermediate claim Hinner: open_interval a b ∈ {open_interval a bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ open_interval a bb) b HbR).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {open_interval aa bb|bb ∈ R}) a (open_interval a b) HaR Hinner).
An exact proof term for the current goal is (basis_in_generated R R_standard_basis (f n0) Hbasis HfInBasis).
We prove the intermediate claim HAcover: A ⊆ ⋃ Fam0.
Let x be given.
Assume HxA: x ∈ A.
We will prove x ∈ ⋃ Fam0.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (HA x HxA).
We prove the intermediate claim Hup: ∃N : set, N ∈ ω ∧ x < N.
Apply (real_E x HxR (∃N : set, N ∈ ω ∧ x < N)) to the current goal.
Assume HxS: SNo x.
Assume Hlev: SNoLev x ∈ ordsucc ω.
Assume HxSNoS: x ∈ SNoS_ (ordsucc ω).
Assume HmOmLt: minus_SNo ω < x.
Assume HxLtOm: x < ω.
Assume Huniq.
Assume Happrox.
An exact proof term for the current goal is (SNoS_ordsucc_omega_bdd_above x HxSNoS HxLtOm).
We prove the intermediate claim Hlow: ∃N : set, N ∈ ω ∧ minus_SNo N < x.
Apply (real_E x HxR (∃N : set, N ∈ ω ∧ minus_SNo N < x)) to the current goal.
Assume HxS: SNo x.
Assume Hlev: SNoLev x ∈ ordsucc ω.
Assume HxSNoS: x ∈ SNoS_ (ordsucc ω).
Assume HmOmLt: minus_SNo ω < x.
Assume HxLtOm: x < ω.
Assume Huniq.
Assume Happrox.
An exact proof term for the current goal is (SNoS_ordsucc_omega_bdd_below x HxSNoS HmOmLt).
Apply Hup to the current goal.
Let Nup be given.
Assume Hupconj.
We prove the intermediate claim HNup: Nup ∈ ω.
An exact proof term for the current goal is (andEL (Nup ∈ ω) (x < Nup) Hupconj).
We prove the intermediate claim HxNup: x < Nup.
An exact proof term for the current goal is (andER (Nup ∈ ω) (x < Nup) Hupconj).
Apply Hlow to the current goal.
Let Nlow be given.
Assume Hlowconj.
We prove the intermediate claim HNlow: Nlow ∈ ω.
An exact proof term for the current goal is (andEL (Nlow ∈ ω) (minus_SNo Nlow < x) Hlowconj).
We prove the intermediate claim HNlowx: minus_SNo Nlow < x.
An exact proof term for the current goal is (andER (Nlow ∈ ω) (minus_SNo Nlow < x) Hlowconj).
Set n to be the term Nup ∪ Nlow.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (omega_binunion Nup Nlow HNup HNlow).
We prove the intermediate claim Hordomega: ordinal ω.
An exact proof term for the current goal is omega_ordinal.
We prove the intermediate claim HordNup: ordinal Nup.
An exact proof term for the current goal is (ordinal_Hered ω Hordomega Nup HNup).
We prove the intermediate claim HordNlow: ordinal Nlow.
An exact proof term for the current goal is (ordinal_Hered ω Hordomega Nlow HNlow).
We prove the intermediate claim Hordn: ordinal n.
An exact proof term for the current goal is (ordinal_Hered ω Hordomega n HnO).
We prove the intermediate claim HNupSub: Nup ⊆ n.
Let t be given.
Assume Ht: t ∈ Nup.
An exact proof term for the current goal is (binunionI1 Nup Nlow t Ht).
We prove the intermediate claim HNlowSub: Nlow ⊆ n.
Let t be given.
Assume Ht: t ∈ Nlow.
An exact proof term for the current goal is (binunionI2 Nup Nlow t Ht).
We prove the intermediate claim HNupLe: Nup ≤ n.
An exact proof term for the current goal is (ordinal_Subq_SNoLe Nup n HordNup Hordn HNupSub).
We prove the intermediate claim HNlowLe: Nlow ≤ n.
An exact proof term for the current goal is (ordinal_Subq_SNoLe Nlow n HordNlow Hordn HNlowSub).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim HNupS: SNo Nup.
An exact proof term for the current goal is (omega_SNo Nup HNup).
We prove the intermediate claim HnS: SNo n.
An exact proof term for the current goal is (omega_SNo n HnO).
We prove the intermediate claim Hxlt_n: x < n.
An exact proof term for the current goal is (SNoLtLe_tra x Nup n HxS HNupS HnS HxNup HNupLe).
We prove the intermediate claim Hn_in_ordsucc: n ∈ ordsucc n.
An exact proof term for the current goal is (ordsuccI2 n).
We prove the intermediate claim Hord_ordsucc: ordinal (ordsucc n).
An exact proof term for the current goal is (ordinal_ordsucc n Hordn).
We prove the intermediate claim Hnlt_ordsucc: n < ordsucc n.
An exact proof term for the current goal is (ordinal_In_SNoLt (ordsucc n) Hord_ordsucc n Hn_in_ordsucc).
We prove the intermediate claim HordS: SNo (ordsucc n).
An exact proof term for the current goal is (omega_SNo (ordsucc n) (omega_ordsucc n HnO)).
We prove the intermediate claim Hxlt_ordsucc: x < ordsucc n.
An exact proof term for the current goal is (SNoLt_tra x n (ordsucc n) HxS HnS HordS Hxlt_n Hnlt_ordsucc).
We prove the intermediate claim HNlowS: SNo Nlow.
An exact proof term for the current goal is (omega_SNo Nlow HNlow).
We prove the intermediate claim Hneg_nS: SNo (minus_SNo n).
An exact proof term for the current goal is (SNo_minus_SNo n HnS).
We prove the intermediate claim Hneg_NlowS: SNo (minus_SNo Nlow).
An exact proof term for the current goal is (SNo_minus_SNo Nlow HNlowS).
We prove the intermediate claim Hle_neg: minus_SNo n ≤ minus_SNo Nlow.
An exact proof term for the current goal is (minus_SNo_Le_contra Nlow n HNlowS HnS HNlowLe).
We prove the intermediate claim Hneglow_lt_x: minus_SNo Nlow < x.
An exact proof term for the current goal is HNlowx.
We prove the intermediate claim Hneg_n_lt_x: minus_SNo n < x.
An exact proof term for the current goal is (SNoLeLt_tra (minus_SNo n) (minus_SNo Nlow) x Hneg_nS Hneg_NlowS HxS Hle_neg Hneglow_lt_x).
We prove the intermediate claim Hnlt_ordsucc_neg: minus_SNo (ordsucc n) < minus_SNo n.
An exact proof term for the current goal is (minus_SNo_Lt_contra n (ordsucc n) HnS HordS Hnlt_ordsucc).
We prove the intermediate claim Hneg_ordsucc_lt_x: minus_SNo (ordsucc n) < x.
An exact proof term for the current goal is (SNoLt_tra (minus_SNo (ordsucc n)) (minus_SNo n) x (SNo_minus_SNo (ordsucc n) HordS) Hneg_nS HxS Hnlt_ordsucc_neg Hneg_n_lt_x).
We prove the intermediate claim HordsuccR: ordsucc n ∈ R.
An exact proof term for the current goal is (ordsucc_in_R n HnO).
We prove the intermediate claim HnegordsuccR: minus_SNo (ordsucc n) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (ordsucc n) HordsuccR).
We prove the intermediate claim HRltL: Rlt (minus_SNo (ordsucc n)) x.
An exact proof term for the current goal is (RltI (minus_SNo (ordsucc n)) x HnegordsuccR HxR Hneg_ordsucc_lt_x).
We prove the intermediate claim HRltR: Rlt x (ordsucc n).
An exact proof term for the current goal is (RltI x (ordsucc n) HxR HordsuccR Hxlt_ordsucc).
We prove the intermediate claim HxIn: x ∈ f n.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt (minus_SNo (ordsucc n)) x0 ∧ Rlt x0 (ordsucc n)) x HxR (andI (Rlt (minus_SNo (ordsucc n)) x) (Rlt x (ordsucc n)) HRltL HRltR)).
We prove the intermediate claim HfnFam: f n ∈ Fam0.
An exact proof term for the current goal is (ReplI ω (λn0 : set ⇒ f n0) n HnO).
An exact proof term for the current goal is (UnionI Fam0 x (f n) HxIn HfnFam).
We prove the intermediate claim Hfincover: has_finite_subcover A R_standard_topology Fam0.
An exact proof term for the current goal is (Hcovprop Fam0 (andI (Fam0 ⊆ R_standard_topology) (A ⊆ ⋃ Fam0) HFam0sub HAcover)).
Apply Hfincover to the current goal.
Let G be given.
Assume HGtriple.
We prove the intermediate claim HGsub: G ⊆ Fam0.
An exact proof term for the current goal is (andEL (G ⊆ Fam0) (finite G) (andEL (G ⊆ Fam0 ∧ finite G) (A ⊆ ⋃ G) HGtriple)).
We prove the intermediate claim HGfin: finite G.
An exact proof term for the current goal is (andER (G ⊆ Fam0) (finite G) (andEL (G ⊆ Fam0 ∧ finite G) (A ⊆ ⋃ G) HGtriple)).
We prove the intermediate claim HAcovG: A ⊆ ⋃ G.
An exact proof term for the current goal is (andER (G ⊆ Fam0 ∧ finite G) (A ⊆ ⋃ G) HGtriple).
Set pickN to be the term λU : set ⇒ Eps_i (λn0 : set ⇒ n0 ∈ ω ∧ U = f n0).
Set Nset to be the term {pickN U|U ∈ G}.
We prove the intermediate claim HNsetFin: finite Nset.
An exact proof term for the current goal is (Repl_finite (λU0 : set ⇒ pickN U0) G HGfin).
We prove the intermediate claim HexA: ∃x : set, x ∈ A.
An exact proof term for the current goal is (nonempty_has_element A HAne).
Apply HexA to the current goal.
Let x0 be given.
Assume Hx0A: x0 ∈ A.
We prove the intermediate claim Hx0UG: x0 ∈ ⋃ G.
An exact proof term for the current goal is (HAcovG x0 Hx0A).
We prove the intermediate claim HexU0: ∃U0 : set, x0 ∈ U0 ∧ U0 ∈ G.
An exact proof term for the current goal is (iffEL (x0 ∈ ⋃ G) (∃Y : set, x0 ∈ Y ∧ Y ∈ G) (UnionEq G x0) Hx0UG).
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0conj.
We prove the intermediate claim HU0G: U0 ∈ G.
An exact proof term for the current goal is (andER (x0 ∈ U0) (U0 ∈ G) HU0conj).
We prove the intermediate claim HU0Fam0: U0 ∈ Fam0.
An exact proof term for the current goal is (HGsub U0 HU0G).
We prove the intermediate claim Hexn0: ∃n0 : set, n0 ∈ ω ∧ U0 = f n0.
An exact proof term for the current goal is (ReplE ω (λn0 : set ⇒ f n0) U0 HU0Fam0).
We prove the intermediate claim HpickU0: pickN U0 ∈ ω ∧ U0 = f (pickN U0).
An exact proof term for the current goal is (Eps_i_ex (λn0 : set ⇒ n0 ∈ ω ∧ U0 = f n0) Hexn0).
We prove the intermediate claim HpickU0O: pickN U0 ∈ ω.
An exact proof term for the current goal is (andEL (pickN U0 ∈ ω) (U0 = f (pickN U0)) HpickU0).
We prove the intermediate claim HNsetNe: Nset ≠ Empty.
Apply (elem_implies_nonempty Nset (pickN U0)) to the current goal.
An exact proof term for the current goal is (ReplI G (λU : set ⇒ pickN U) U0 HU0G).
We prove the intermediate claim HAllSNo: ∀y ∈ Nset, SNo y.
Let y be given.
Assume Hy: y ∈ Nset.
Apply (ReplE_impred G (λU : set ⇒ pickN U) y Hy (SNo y)) to the current goal.
Let U be given.
Assume HU: U ∈ G.
Assume Hey: y = pickN U.
rewrite the current goal using Hey (from left to right).
We prove the intermediate claim HUfam: U ∈ Fam0.
An exact proof term for the current goal is (HGsub U HU).
We prove the intermediate claim Hexn: ∃n0 : set, n0 ∈ ω ∧ U = f n0.
An exact proof term for the current goal is (ReplE ω (λn0 : set ⇒ f n0) U HUfam).
We prove the intermediate claim Hpick: pickN U ∈ ω ∧ U = f (pickN U).
An exact proof term for the current goal is (Eps_i_ex (λn0 : set ⇒ n0 ∈ ω ∧ U = f n0) Hexn).
We prove the intermediate claim HpickO: pickN U ∈ ω.
An exact proof term for the current goal is (andEL (pickN U ∈ ω) (U = f (pickN U)) Hpick).
An exact proof term for the current goal is (omega_SNo (pickN U) HpickO).
We prove the intermediate claim Hexmax: ∃nmax : set, SNo_max_of Nset nmax.
An exact proof term for the current goal is (finite_max_exists Nset (λy Hy ⇒ HAllSNo y Hy) HNsetFin HNsetNe).
Apply Hexmax to the current goal.
Let nmax be given.
Assume Hmax.
We prove the intermediate claim HnmaxIn: nmax ∈ Nset.
An exact proof term for the current goal is (andEL (nmax ∈ Nset) (SNo nmax) (andEL (nmax ∈ Nset ∧ SNo nmax) (∀y ∈ Nset, SNo y → y ≤ nmax) Hmax)).
We prove the intermediate claim HnmaxS: SNo nmax.
An exact proof term for the current goal is (andER (nmax ∈ Nset) (SNo nmax) (andEL (nmax ∈ Nset ∧ SNo nmax) (∀y ∈ Nset, SNo y → y ≤ nmax) Hmax)).
We prove the intermediate claim Hmaxprop: ∀y ∈ Nset, SNo y → y ≤ nmax.
An exact proof term for the current goal is (andER (nmax ∈ Nset ∧ SNo nmax) (∀y ∈ Nset, SNo y → y ≤ nmax) Hmax).
Set M to be the term ordsucc nmax.
We use M to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HnmaxO: nmax ∈ ω.
Apply (ReplE_impred G (λU : set ⇒ pickN U) nmax HnmaxIn (nmax ∈ ω)) to the current goal.
Let U be given.
Assume HU: U ∈ G.
Assume Heq: nmax = pickN U.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HUfam: U ∈ Fam0.
An exact proof term for the current goal is (HGsub U HU).
We prove the intermediate claim Hexn: ∃n0 : set, n0 ∈ ω ∧ U = f n0.
An exact proof term for the current goal is (ReplE ω (λn0 : set ⇒ f n0) U HUfam).
We prove the intermediate claim Hpick: pickN U ∈ ω ∧ U = f (pickN U).
An exact proof term for the current goal is (Eps_i_ex (λn0 : set ⇒ n0 ∈ ω ∧ U = f n0) Hexn).
An exact proof term for the current goal is (andEL (pickN U ∈ ω) (U = f (pickN U)) Hpick).
An exact proof term for the current goal is (ordsucc_in_R nmax HnmaxO).
Let x be given.
Assume HxA: x ∈ A.
We will prove ¬ (Rlt M (Abs x)).
We prove the intermediate claim HxUG: x ∈ ⋃ G.
An exact proof term for the current goal is (HAcovG x HxA).
We prove the intermediate claim HexU: ∃U : set, x ∈ U ∧ U ∈ G.
An exact proof term for the current goal is (iffEL (x ∈ ⋃ G) (∃Y : set, x ∈ Y ∧ Y ∈ G) (UnionEq G x) HxUG).
Apply HexU to the current goal.
Let U be given.
Assume HUconj.
We prove the intermediate claim HUinG: U ∈ G.
An exact proof term for the current goal is (andER (x ∈ U) (U ∈ G) HUconj).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (U ∈ G) HUconj).
We prove the intermediate claim HUfam: U ∈ Fam0.
An exact proof term for the current goal is (HGsub U HUinG).
We prove the intermediate claim Hexn: ∃n0 : set, n0 ∈ ω ∧ U = f n0.
An exact proof term for the current goal is (ReplE ω (λn0 : set ⇒ f n0) U HUfam).
We prove the intermediate claim Hpick: pickN U ∈ ω ∧ U = f (pickN U).
An exact proof term for the current goal is (Eps_i_ex (λn0 : set ⇒ n0 ∈ ω ∧ U = f n0) Hexn).
We prove the intermediate claim HnU: pickN U ∈ ω.
An exact proof term for the current goal is (andEL (pickN U ∈ ω) (U = f (pickN U)) Hpick).
We prove the intermediate claim HUeq: U = f (pickN U).
An exact proof term for the current goal is (andER (pickN U ∈ ω) (U = f (pickN U)) Hpick).
We prove the intermediate claim HNin: pickN U ∈ Nset.
An exact proof term for the current goal is (ReplI G (λU0 : set ⇒ pickN U0) U HUinG).
We prove the intermediate claim HNle: pickN U ≤ nmax.
An exact proof term for the current goal is (Hmaxprop (pickN U) HNin (omega_SNo (pickN U) HnU)).
We prove the intermediate claim HordsuccLe: ordsucc (pickN U) ≤ M.
We prove the intermediate claim HnU_S: SNo (pickN U).
An exact proof term for the current goal is (omega_SNo (pickN U) HnU).
We prove the intermediate claim HnmaxO: nmax ∈ ω.
Apply (ReplE_impred G (λU0 : set ⇒ pickN U0) nmax HnmaxIn (nmax ∈ ω)) to the current goal.
Let U1 be given.
Assume HU1: U1 ∈ G.
Assume Heq: nmax = pickN U1.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HU1fam: U1 ∈ Fam0.
An exact proof term for the current goal is (HGsub U1 HU1).
We prove the intermediate claim Hexn1: ∃n0 : set, n0 ∈ ω ∧ U1 = f n0.
An exact proof term for the current goal is (ReplE ω (λn0 : set ⇒ f n0) U1 HU1fam).
We prove the intermediate claim Hpick1: pickN U1 ∈ ω ∧ U1 = f (pickN U1).
An exact proof term for the current goal is (Eps_i_ex (λn0 : set ⇒ n0 ∈ ω ∧ U1 = f n0) Hexn1).
An exact proof term for the current goal is (andEL (pickN U1 ∈ ω) (U1 = f (pickN U1)) Hpick1).
We prove the intermediate claim Hnmax_S: SNo nmax.
An exact proof term for the current goal is (omega_SNo nmax HnmaxO).
We prove the intermediate claim H1S: SNo 1.
An exact proof term for the current goal is SNo_1.
We prove the intermediate claim Hadd: add_SNo (pickN U) 1 ≤ add_SNo nmax 1.
An exact proof term for the current goal is (add_SNo_Le1 (pickN U) 1 nmax HnU_S H1S Hnmax_S HNle).
We prove the intermediate claim Hm1: add_SNo (pickN U) 1 = ordsucc (pickN U).
An exact proof term for the current goal is (add_SNo_1_ordsucc (pickN U) HnU).
We prove the intermediate claim Hm2: add_SNo nmax 1 = ordsucc nmax.
An exact proof term for the current goal is (add_SNo_1_ordsucc nmax HnmaxO).
rewrite the current goal using Hm1 (from right to left).
rewrite the current goal using Hm2 (from right to left).
An exact proof term for the current goal is Hadd.
We prove the intermediate claim HxUfn: x ∈ f (pickN U).
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HxU.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (HA x HxA).
We prove the intermediate claim Hxconj: Rlt (minus_SNo (ordsucc (pickN U))) x ∧ Rlt x (ordsucc (pickN U)).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (minus_SNo (ordsucc (pickN U))) x0 ∧ Rlt x0 (ordsucc (pickN U))) x HxUfn).
We prove the intermediate claim HxL: Rlt (minus_SNo (ordsucc (pickN U))) x.
An exact proof term for the current goal is (andEL (Rlt (minus_SNo (ordsucc (pickN U))) x) (Rlt x (ordsucc (pickN U))) Hxconj).
We prove the intermediate claim HxRgt: Rlt x (ordsucc (pickN U)).
An exact proof term for the current goal is (andER (Rlt (minus_SNo (ordsucc (pickN U))) x) (Rlt x (ordsucc (pickN U))) Hxconj).
We prove the intermediate claim HNsetSubOmega: Nset ⊆ ω.
Let y be given.
Assume Hy: y ∈ Nset.
Apply (ReplE_impred G (λU0 : set ⇒ pickN U0) y Hy (y ∈ ω)) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ G.
Assume Hey: y = pickN U0.
rewrite the current goal using Hey (from left to right).
We prove the intermediate claim HU0fam: U0 ∈ Fam0.
An exact proof term for the current goal is (HGsub U0 HU0).
We prove the intermediate claim Hexn0: ∃n0 : set, n0 ∈ ω ∧ U0 = f n0.
An exact proof term for the current goal is (ReplE ω (λn0 : set ⇒ f n0) U0 HU0fam).
We prove the intermediate claim Hpick0: pickN U0 ∈ ω ∧ U0 = f (pickN U0).
An exact proof term for the current goal is (Eps_i_ex (λn0 : set ⇒ n0 ∈ ω ∧ U0 = f n0) Hexn0).
An exact proof term for the current goal is (andEL (pickN U0 ∈ ω) (U0 = f (pickN U0)) Hpick0).
We prove the intermediate claim HnmaxO: nmax ∈ ω.
An exact proof term for the current goal is (HNsetSubOmega nmax HnmaxIn).
We prove the intermediate claim HM: M ∈ R.
An exact proof term for the current goal is (ordsucc_in_R nmax HnmaxO).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim HM_S: SNo M.
An exact proof term for the current goal is (real_SNo M HM).
We prove the intermediate claim HmU: ordsucc (pickN U) ∈ R.
An exact proof term for the current goal is (ordsucc_in_R (pickN U) HnU).
We prove the intermediate claim HmU_S: SNo (ordsucc (pickN U)).
An exact proof term for the current goal is (omega_SNo (ordsucc (pickN U)) (omega_ordsucc (pickN U) HnU)).
We prove the intermediate claim HxltmU: x < ordsucc (pickN U).
An exact proof term for the current goal is (RltE_lt x (ordsucc (pickN U)) HxRgt).
We prove the intermediate claim HxltM: x < M.
An exact proof term for the current goal is (SNoLtLe_tra x (ordsucc (pickN U)) M HxS HmU_S HM_S HxltmU HordsuccLe).
We prove the intermediate claim HRltxM: Rlt x M.
An exact proof term for the current goal is (RltI x M HxR HM HxltM).
We prove the intermediate claim HnegM_R: minus_SNo M ∈ R.
An exact proof term for the current goal is (real_minus_SNo M HM).
We prove the intermediate claim HnegM_S: SNo (minus_SNo M).
An exact proof term for the current goal is (SNo_minus_SNo M HM_S).
We prove the intermediate claim HnegmU_S: SNo (minus_SNo (ordsucc (pickN U))).
An exact proof term for the current goal is (SNo_minus_SNo (ordsucc (pickN U)) HmU_S).
We prove the intermediate claim Hxgt_negmU: minus_SNo (ordsucc (pickN U)) < x.
An exact proof term for the current goal is (RltE_lt (minus_SNo (ordsucc (pickN U))) x HxL).
We prove the intermediate claim Hle_neg: minus_SNo M ≤ minus_SNo (ordsucc (pickN U)).
An exact proof term for the current goal is (minus_SNo_Le_contra (ordsucc (pickN U)) M HmU_S HM_S HordsuccLe).
We prove the intermediate claim HnegM_lt_x: minus_SNo M < x.
An exact proof term for the current goal is (SNoLeLt_tra (minus_SNo M) (minus_SNo (ordsucc (pickN U))) x HnegM_S HnegmU_S HxS Hle_neg Hxgt_negmU).
We prove the intermediate claim HRltnegMx: Rlt (minus_SNo M) x.
An exact proof term for the current goal is (RltI (minus_SNo M) x HnegM_R HxR HnegM_lt_x).
An exact proof term for the current goal is (interval_bounds_Abs M x HM HxR HRltnegMx HRltxM).
∎