Let Fam be given.
Assume Hcover: open_cover_of unit_interval unit_interval_topology Fam.
We will prove has_finite_subcover unit_interval unit_interval_topology Fam.
We prove the intermediate claim HtopI: topology_on unit_interval unit_interval_topology.
An exact proof term for the current goal is (open_cover_of_topology unit_interval unit_interval_topology Fam Hcover).
We prove the intermediate claim HIcov: unit_interval ⊆ ⋃ Fam.
An exact proof term for the current goal is (open_cover_of_covers unit_interval unit_interval_topology Fam Hcover).
We prove the intermediate claim HmemOpen: ∀U : set, U ∈ Fam → U ∈ unit_interval_topology.
Let U be given.
Assume HU: U ∈ Fam.
An exact proof term for the current goal is (open_cover_of_members_open unit_interval unit_interval_topology Fam U Hcover HU).
Set prefix to be the term λa : set ⇒ {x ∈ unit_interval|Rle x a}.
Set Good to be the term {a ∈ unit_interval|∃G : set, (G ⊆ Fam ∧ finite G ∧ (prefix a) ⊆ ⋃ G)}.
We prove the intermediate claim H0I: 0 ∈ unit_interval.
An exact proof term for the current goal is zero_in_unit_interval.
We prove the intermediate claim H0Good: 0 ∈ Good.
We prove the intermediate claim Hex0: ∃G : set, (G ⊆ Fam ∧ finite G ∧ (prefix 0) ⊆ ⋃ G).
We prove the intermediate claim H0inUnionFam: 0 ∈ ⋃ Fam.
An exact proof term for the current goal is (HIcov 0 H0I).
Apply (UnionE_impred Fam 0 H0inUnionFam) to the current goal.
Let U0 be given.
Assume H0U0: 0 ∈ U0.
Assume HU0Fam: U0 ∈ Fam.
We use {U0} to witness the existential quantifier.
We will prove {U0} ⊆ Fam ∧ finite {U0} ∧ (prefix 0) ⊆ ⋃ {U0}.
Apply andI to the current goal.
Apply andI to the current goal.
Let U be given.
Assume HU: U ∈ {U0}.
We will prove U ∈ Fam.
We prove the intermediate claim HUeq: U = U0.
An exact proof term for the current goal is (SingE U0 U HU).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is HU0Fam.
An exact proof term for the current goal is (Sing_finite U0).
Let x be given.
Assume Hx: x ∈ prefix 0.
We will prove x ∈ ⋃ {U0}.
We prove the intermediate claim HprefDef: prefix 0 = {x0 ∈ unit_interval|Rle x0 0}.
Use reflexivity.
We prove the intermediate claim HxSep: x ∈ {x0 ∈ unit_interval|Rle x0 0}.
rewrite the current goal using HprefDef (from right to left).
An exact proof term for the current goal is Hx.
We prove the intermediate claim HxI: x ∈ unit_interval.
An exact proof term for the current goal is (SepE1 unit_interval (λx0 : set ⇒ Rle x0 0) x HxSep).
We prove the intermediate claim Hxle0: Rle x 0.
An exact proof term for the current goal is (SepE2 unit_interval (λx0 : set ⇒ Rle x0 0) x HxSep).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R x HxI).
We prove the intermediate claim Hxprop: ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x).
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) x HxI).
We prove the intermediate claim Hnltx0: ¬ (Rlt x 0).
An exact proof term for the current goal is (andEL (¬ (Rlt x 0)) (¬ (Rlt 1 x)) Hxprop).
We prove the intermediate claim H0lex: Rle 0 x.
An exact proof term for the current goal is (RleI 0 x real_0 HxR Hnltx0).
We prove the intermediate claim Hxeq0: x = 0.
An exact proof term for the current goal is (Rle_antisym x 0 Hxle0 H0lex).
rewrite the current goal using Hxeq0 (from left to right).
An exact proof term for the current goal is (UnionI {U0} 0 U0 H0U0 (SingI U0)).
An exact proof term for the current goal is (SepI unit_interval (λa0 : set ⇒ ∃G : set, (G ⊆ Fam ∧ finite G ∧ (prefix a0) ⊆ ⋃ G)) 0 H0I Hex0).
We prove the intermediate claim HGoodHasElem: ∃a0 : set, a0 ∈ Good.
We use 0 to witness the existential quantifier.
An exact proof term for the current goal is H0Good.
We prove the intermediate claim HGoodInR: ∀a : set, a ∈ Good → a ∈ R.
Let a be given.
Assume Ha: a ∈ Good.
We prove the intermediate claim HaI: a ∈ unit_interval.
An exact proof term for the current goal is (SepE1 unit_interval (λa0 : set ⇒ ∃G : set, (G ⊆ Fam ∧ finite G ∧ (prefix a0) ⊆ ⋃ G)) a Ha).
An exact proof term for the current goal is (unit_interval_sub_R a HaI).
We prove the intermediate claim HGoodUB: ∃u : set, u ∈ R ∧ ∀a : set, a ∈ Good → a ∈ R → Rle a u.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is real_1.
Let a be given.
Assume HaG: a ∈ Good.
Assume HaR: a ∈ R.
We will prove Rle a 1.
We prove the intermediate claim HaI: a ∈ unit_interval.
An exact proof term for the current goal is (SepE1 unit_interval (λa0 : set ⇒ ∃G : set, (G ⊆ Fam ∧ finite G ∧ (prefix a0) ⊆ ⋃ G)) a HaG).
We prove the intermediate claim HaProp: ¬ (Rlt a 0) ∧ ¬ (Rlt 1 a).
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) a HaI).
We prove the intermediate claim Hnlt1a: ¬ (Rlt 1 a).
An exact proof term for the current goal is (andER (¬ (Rlt a 0)) (¬ (Rlt 1 a)) HaProp).
An exact proof term for the current goal is (RleI a 1 HaR real_1 Hnlt1a).
We prove the intermediate claim Hexlub: ∃l : set, R_lub Good l.
An exact proof term for the current goal is (R_lub_exists Good HGoodHasElem HGoodInR HGoodUB).
Apply Hexlub to the current goal.
Let l be given.
Assume Hlub: R_lub Good l.
We prove the intermediate claim HlR: l ∈ R.
An exact proof term for the current goal is (R_lub_in_R Good l Hlub).
We prove the intermediate claim Hl_ge0: Rle 0 l.
We prove the intermediate claim Hcore: l ∈ R ∧ (∀a : set, a ∈ Good → a ∈ R → Rle a l).
An exact proof term for the current goal is (andEL (l ∈ R ∧ (∀a : set, a ∈ Good → a ∈ R → Rle a l)) (∀u : set, u ∈ R → (∀a : set, a ∈ Good → a ∈ R → Rle a u) → Rle l u) Hlub).
We prove the intermediate claim HlUB: ∀a : set, a ∈ Good → a ∈ R → Rle a l.
An exact proof term for the current goal is (andER (l ∈ R) (∀a : set, a ∈ Good → a ∈ R → Rle a l) Hcore).
An exact proof term for the current goal is (HlUB 0 H0Good real_0).
We prove the intermediate claim Hl_le1: Rle l 1.
We prove the intermediate claim Hlmin: ∀u : set, u ∈ R → (∀a : set, a ∈ Good → a ∈ R → Rle a u) → Rle l u.
An exact proof term for the current goal is (andER (l ∈ R ∧ (∀a : set, a ∈ Good → a ∈ R → Rle a l)) (∀u : set, u ∈ R → (∀a : set, a ∈ Good → a ∈ R → Rle a u) → Rle l u) Hlub).
We prove the intermediate claim H1ub2: ∀a : set, a ∈ Good → a ∈ R → Rle a 1.
Let a be given.
Assume HaG: a ∈ Good.
Assume HaR: a ∈ R.
We prove the intermediate claim HaI: a ∈ unit_interval.
An exact proof term for the current goal is (SepE1 unit_interval (λa0 : set ⇒ ∃G : set, (G ⊆ Fam ∧ finite G ∧ (prefix a0) ⊆ ⋃ G)) a HaG).
We prove the intermediate claim HaProp: ¬ (Rlt a 0) ∧ ¬ (Rlt 1 a).
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) a HaI).
We prove the intermediate claim Hnlt1a: ¬ (Rlt 1 a).
An exact proof term for the current goal is (andER (¬ (Rlt a 0)) (¬ (Rlt 1 a)) HaProp).
An exact proof term for the current goal is (RleI a 1 HaR real_1 Hnlt1a).
An exact proof term for the current goal is (Hlmin 1 real_1 H1ub2).
We prove the intermediate claim HlI: l ∈ unit_interval.
Apply (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) l HlR) to the current goal.
Apply andI to the current goal.
Assume Hlt: Rlt l 0.
We will prove False.
An exact proof term for the current goal is ((RleE_nlt 0 l Hl_ge0) Hlt).
Assume Hlt: Rlt 1 l.
We will prove False.
We prove the intermediate claim Hnlt: ¬ (Rlt 1 l).
An exact proof term for the current goal is (RleE_nlt l 1 Hl_le1).
An exact proof term for the current goal is (Hnlt Hlt).
We prove the intermediate claim Hprefix1: prefix 1 = unit_interval.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ prefix 1.
An exact proof term for the current goal is (SepE1 unit_interval (λx0 : set ⇒ Rle x0 1) x Hx).
Let x be given.
Assume Hx: x ∈ unit_interval.
We will prove x ∈ prefix 1.
We prove the intermediate claim HprefDef: prefix 1 = {x0 ∈ unit_interval|Rle x0 1}.
Use reflexivity.
rewrite the current goal using HprefDef (from left to right).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R x Hx).
We prove the intermediate claim Hxprop: ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x).
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) x Hx).
We prove the intermediate claim Hnlt1x: ¬ (Rlt 1 x).
An exact proof term for the current goal is (andER (¬ (Rlt x 0)) (¬ (Rlt 1 x)) Hxprop).
Apply (SepI unit_interval (λx0 : set ⇒ Rle x0 1) x Hx) to the current goal.
An exact proof term for the current goal is (RleI x 1 HxR real_1 Hnlt1x).
We prove the intermediate claim Hfinish: 1 ∈ Good → has_finite_subcover unit_interval unit_interval_topology Fam.
Assume H1G: 1 ∈ Good.
We prove the intermediate claim HexG: ∃G : set, (G ⊆ Fam ∧ finite G ∧ (prefix 1) ⊆ ⋃ G).
An exact proof term for the current goal is (SepE2 unit_interval (λa0 : set ⇒ ∃G : set, (G ⊆ Fam ∧ finite G ∧ (prefix a0) ⊆ ⋃ G)) 1 H1G).
Apply HexG to the current goal.
Let G be given.
Assume HGtriple.
We prove the intermediate claim HG12: G ⊆ Fam ∧ finite G.
An exact proof term for the current goal is (andEL (G ⊆ Fam ∧ finite G) ((prefix 1) ⊆ ⋃ G) HGtriple).
We prove the intermediate claim HGsub: G ⊆ Fam.
An exact proof term for the current goal is (andEL (G ⊆ Fam) (finite G) HG12).
We prove the intermediate claim HGfin: finite G.
An exact proof term for the current goal is (andER (G ⊆ Fam) (finite G) HG12).
We prove the intermediate claim HcovPref: (prefix 1) ⊆ ⋃ G.
An exact proof term for the current goal is (andER (G ⊆ Fam ∧ finite G) ((prefix 1) ⊆ ⋃ G) HGtriple).
We will prove has_finite_subcover unit_interval unit_interval_topology Fam.
We prove the intermediate claim HcovX: unit_interval ⊆ ⋃ G.
Let x be given.
Assume HxI: x ∈ unit_interval.
We will prove x ∈ ⋃ G.
We prove the intermediate claim HxP: x ∈ prefix 1.
rewrite the current goal using Hprefix1 (from left to right).
An exact proof term for the current goal is HxI.
An exact proof term for the current goal is (HcovPref x HxP).
We prove the intermediate claim HGtriple2: G ⊆ Fam ∧ finite G ∧ unit_interval ⊆ ⋃ G.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HGsub.
An exact proof term for the current goal is HGfin.
An exact proof term for the current goal is HcovX.
An exact proof term for the current goal is (has_finite_subcoverI unit_interval unit_interval_topology Fam G HGtriple2).
We prove the intermediate claim H1G: 1 ∈ Good.
We prove the intermediate claim HlUnionFam: l ∈ ⋃ Fam.
An exact proof term for the current goal is (HIcov l HlI).
Apply (UnionE_impred Fam l HlUnionFam (1 ∈ Good)) to the current goal.
Let U0 be given.
Assume HlU0: l ∈ U0.
Assume HU0Fam: U0 ∈ Fam.
We prove the intermediate claim HU0Tx: U0 ∈ unit_interval_topology.
An exact proof term for the current goal is (HmemOpen U0 HU0Fam).
We prove the intermediate claim HU0subI: U0 ⊆ unit_interval.
An exact proof term for the current goal is (topology_elem_subset unit_interval unit_interval_topology U0 unit_interval_topology_on HU0Tx).
We prove the intermediate claim HU0open_in: open_in unit_interval unit_interval_topology U0.
An exact proof term for the current goal is (open_inI unit_interval unit_interval_topology U0 unit_interval_topology_on HU0Tx).
We prove the intermediate claim HexV: ∃V ∈ R_standard_topology, U0 = V ∩ unit_interval.
An exact proof term for the current goal is (iffEL (open_in unit_interval unit_interval_topology U0) (∃V ∈ R_standard_topology, U0 = V ∩ unit_interval) (open_in_subspace_iff R R_standard_topology unit_interval U0 R_standard_topology_is_topology unit_interval_sub_R HU0subI) HU0open_in).
Apply HexV to the current goal.
Let V be given.
Assume HVpair.
We prove the intermediate claim HVopen: V ∈ R_standard_topology.
An exact proof term for the current goal is (andEL (V ∈ R_standard_topology) (U0 = V ∩ unit_interval) HVpair).
We prove the intermediate claim HU0eq: U0 = V ∩ unit_interval.
An exact proof term for the current goal is (andER (V ∈ R_standard_topology) (U0 = V ∩ unit_interval) HVpair).
We prove the intermediate claim HlV: l ∈ V.
We prove the intermediate claim Hlcap: l ∈ V ∩ unit_interval.
rewrite the current goal using HU0eq (from right to left).
An exact proof term for the current goal is HlU0.
An exact proof term for the current goal is (binintersectE1 V unit_interval l Hlcap).
We prove the intermediate claim Hexcd: ∃c d : set, c ∈ R ∧ d ∈ R ∧ l ∈ open_interval c d ∧ open_interval c d ⊆ V ∧ Rlt c l ∧ Rlt l d.
An exact proof term for the current goal is (R_standard_open_refine_interval V l HVopen HlV).
Apply Hexcd to the current goal.
Let c be given.
Assume Hexd.
Apply Hexd to the current goal.
Let d be given.
Assume Hcdpack.
We prove the intermediate claim Hcd1: ((((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) ∧ open_interval c d ⊆ V) ∧ Rlt c l).
An exact proof term for the current goal is (andEL ((((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) ∧ open_interval c d ⊆ V) ∧ Rlt c l) (Rlt l d) Hcdpack).
We prove the intermediate claim Hld: Rlt l d.
An exact proof term for the current goal is (andER ((((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) ∧ open_interval c d ⊆ V) ∧ Rlt c l) (Rlt l d) Hcdpack).
We prove the intermediate claim Hcd2: (((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) ∧ open_interval c d ⊆ V).
An exact proof term for the current goal is (andEL (((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) ∧ open_interval c d ⊆ V) (Rlt c l) Hcd1).
We prove the intermediate claim Hcl: Rlt c l.
An exact proof term for the current goal is (andER (((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) ∧ open_interval c d ⊆ V) (Rlt c l) Hcd1).
We prove the intermediate claim Hcd3: (c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d.
An exact proof term for the current goal is (andEL ((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) (open_interval c d ⊆ V) Hcd2).
We prove the intermediate claim HIntSubV: open_interval c d ⊆ V.
An exact proof term for the current goal is (andER ((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) (open_interval c d ⊆ V) Hcd2).
We prove the intermediate claim Hcd4: c ∈ R ∧ d ∈ R.
An exact proof term for the current goal is (andEL (c ∈ R ∧ d ∈ R) (l ∈ open_interval c d) Hcd3).
We prove the intermediate claim HlInt: l ∈ open_interval c d.
An exact proof term for the current goal is (andER (c ∈ R ∧ d ∈ R) (l ∈ open_interval c d) Hcd3).
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (andEL (c ∈ R) (d ∈ R) Hcd4).
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (andER (c ∈ R) (d ∈ R) Hcd4).
Set gap to be the term add_SNo l (minus_SNo c).
We prove the intermediate claim HgapR: gap ∈ R.
An exact proof term for the current goal is (real_add_SNo l HlR (minus_SNo c) (real_minus_SNo c HcR)).
We prove the intermediate claim HgapPos: Rlt 0 gap.
An exact proof term for the current goal is (Rlt_0_diff_of_lt c l Hcl).
We prove the intermediate claim HgapS: SNo gap.
An exact proof term for the current goal is (real_SNo gap HgapR).
We prove the intermediate claim HgapPosS: 0 < gap.
An exact proof term for the current goal is (RltE_lt 0 gap HgapPos).
We prove the intermediate claim He1S: SNo (eps_ 1).
An exact proof term for the current goal is SNo_eps_1.
We prove the intermediate claim He1PosS: 0 < (eps_ 1).
An exact proof term for the current goal is (RltE_lt 0 (eps_ 1) eps_1_pos_R).
Set eps to be the term mul_SNo (eps_ 1) gap.
We prove the intermediate claim HepsR: eps ∈ R.
An exact proof term for the current goal is (real_mul_SNo (eps_ 1) eps_1_in_R gap HgapR).
We prove the intermediate claim HepsS: SNo eps.
An exact proof term for the current goal is (real_SNo eps HepsR).
We prove the intermediate claim HepsPosS: 0 < eps.
An exact proof term for the current goal is (mul_SNo_pos_pos (eps_ 1) gap He1S HgapS He1PosS HgapPosS).
We prove the intermediate claim HepsPos: Rlt 0 eps.
An exact proof term for the current goal is (RltI 0 eps real_0 HepsR HepsPosS).
We prove the intermediate claim Hexa: ∃a : set, a ∈ Good ∧ a ∈ R ∧ Rlt (add_SNo l (minus_SNo eps)) a.
An exact proof term for the current goal is (R_lub_approx_from_below Good l eps Hlub HepsR HepsPos).
Apply Hexa to the current goal.
Let a be given.
Assume Hapack.
We prove the intermediate claim Hapair: a ∈ Good ∧ a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ Good ∧ a ∈ R) (Rlt (add_SNo l (minus_SNo eps)) a) Hapack).
We prove the intermediate claim HaG: a ∈ Good.
An exact proof term for the current goal is (andEL (a ∈ Good) (a ∈ R) Hapair).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andER (a ∈ Good) (a ∈ R) Hapair).
We prove the intermediate claim Hlt_lmeps_a: Rlt (add_SNo l (minus_SNo eps)) a.
An exact proof term for the current goal is (andER (a ∈ Good ∧ a ∈ R) (Rlt (add_SNo l (minus_SNo eps)) a) Hapack).
We prove the intermediate claim HaI: a ∈ unit_interval.
An exact proof term for the current goal is (SepE1 unit_interval (λa0 : set ⇒ ∃G : set, (G ⊆ Fam ∧ finite G ∧ (prefix a0) ⊆ ⋃ G)) a HaG).
We prove the intermediate claim Hale_l: Rle a l.
We prove the intermediate claim Hcore: l ∈ R ∧ (∀a0 : set, a0 ∈ Good → a0 ∈ R → Rle a0 l).
An exact proof term for the current goal is (andEL (l ∈ R ∧ (∀a0 : set, a0 ∈ Good → a0 ∈ R → Rle a0 l)) (∀u : set, u ∈ R → (∀a0 : set, a0 ∈ Good → a0 ∈ R → Rle a0 u) → Rle l u) Hlub).
We prove the intermediate claim Hub: ∀a0 : set, a0 ∈ Good → a0 ∈ R → Rle a0 l.
An exact proof term for the current goal is (andER (l ∈ R) (∀a0 : set, a0 ∈ Good → a0 ∈ R → Rle a0 l) Hcore).
An exact proof term for the current goal is (Hub a HaG HaR).
We prove the intermediate claim HlmEpsR: add_SNo l (minus_SNo eps) ∈ R.
An exact proof term for the current goal is (real_add_SNo l HlR (minus_SNo eps) (real_minus_SNo eps HepsR)).
We prove the intermediate claim HlS: SNo l.
An exact proof term for the current goal is (real_SNo l HlR).
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
We prove the intermediate claim HepsLtGap: eps < gap.
We prove the intermediate claim He1lt1: (eps_ 1) < 1.
An exact proof term for the current goal is (RltE_lt (eps_ 1) 1 eps_1_lt1_R).
An exact proof term for the current goal is (mul_SNo_Lt1_pos_Lt (eps_ 1) gap He1S HgapS He1lt1 HgapPosS).
We prove the intermediate claim HcEpsLt: add_SNo c eps < add_SNo c gap.
An exact proof term for the current goal is (add_SNo_Lt2 c eps gap HcS HepsS HgapS HepsLtGap).
We prove the intermediate claim HcGapEq: add_SNo c gap = l.
We prove the intermediate claim Hassoc1: add_SNo c (add_SNo l (minus_SNo c)) = add_SNo (add_SNo c l) (minus_SNo c).
An exact proof term for the current goal is (add_SNo_assoc c l (minus_SNo c) HcS HlS (SNo_minus_SNo c HcS)).
We prove the intermediate claim Hcom1: add_SNo c l = add_SNo l c.
An exact proof term for the current goal is (add_SNo_com c l HcS HlS).
We prove the intermediate claim Hassoc2: add_SNo l (add_SNo c (minus_SNo c)) = add_SNo (add_SNo l c) (minus_SNo c).
An exact proof term for the current goal is (add_SNo_assoc l c (minus_SNo c) HlS HcS (SNo_minus_SNo c HcS)).
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using Hcom1 (from left to right).
rewrite the current goal using Hassoc2 (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv c HcS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R l HlS).
We prove the intermediate claim HcEpsLtL: add_SNo c eps < l.
rewrite the current goal using HcGapEq (from right to left) at position 2.
An exact proof term for the current goal is HcEpsLt.
We prove the intermediate claim HcLtLmEpsS: c < add_SNo l (minus_SNo eps).
We prove the intermediate claim HmEpsS: SNo (minus_SNo eps).
An exact proof term for the current goal is (SNo_minus_SNo eps HepsS).
We prove the intermediate claim HcEpsS: SNo (add_SNo c eps).
An exact proof term for the current goal is (SNo_add_SNo c eps HcS HepsS).
rewrite the current goal using (add_SNo_0R c HcS) (from right to left) at position 1.
rewrite the current goal using (add_SNo_minus_SNo_rinv eps HepsS) (from right to left) at position 1.
rewrite the current goal using (add_SNo_assoc c eps (minus_SNo eps) HcS HepsS HmEpsS) (from left to right) at position 1.
An exact proof term for the current goal is (add_SNo_Lt1 (add_SNo c eps) (minus_SNo eps) l HcEpsS HmEpsS HlS HcEpsLtL).
We prove the intermediate claim HcLtLmEps: Rlt c (add_SNo l (minus_SNo eps)).
An exact proof term for the current goal is (RltI c (add_SNo l (minus_SNo eps)) HcR HlmEpsR HcLtLmEpsS).
We prove the intermediate claim HcLtA: Rlt c a.
An exact proof term for the current goal is (Rlt_tra c (add_SNo l (minus_SNo eps)) a HcLtLmEps Hlt_lmeps_a).
We prove the intermediate claim Haltd: Rlt a d.
An exact proof term for the current goal is (Rle_Rlt_tra a l d Hale_l Hld).
We prove the intermediate claim HaInt: a ∈ open_interval c d.
We prove the intermediate claim HopenDef: open_interval c d = {z ∈ R|Rlt c z ∧ Rlt z d}.
Use reflexivity.
rewrite the current goal using HopenDef (from left to right).
Apply (SepI R (λz : set ⇒ Rlt c z ∧ Rlt z d) a HaR) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HcLtA.
An exact proof term for the current goal is Haltd.
We prove the intermediate claim HaV: a ∈ V.
An exact proof term for the current goal is (HIntSubV a HaInt).
We prove the intermediate claim HaU0: a ∈ U0.
rewrite the current goal using HU0eq (from left to right).
An exact proof term for the current goal is (binintersectI V unit_interval a HaV HaI).
We prove the intermediate claim HexGpre: ∃Gpre : set, (Gpre ⊆ Fam ∧ finite Gpre ∧ (prefix a) ⊆ ⋃ Gpre).
An exact proof term for the current goal is (SepE2 unit_interval (λa0 : set ⇒ ∃G : set, (G ⊆ Fam ∧ finite G ∧ (prefix a0) ⊆ ⋃ G)) a HaG).
Apply HexGpre to the current goal.
Let Gpre be given.
Assume HGpre.
We prove the intermediate claim HGpreLeft: (Gpre ⊆ Fam ∧ finite Gpre).
An exact proof term for the current goal is (andEL (Gpre ⊆ Fam ∧ finite Gpre) ((prefix a) ⊆ ⋃ Gpre) HGpre).
We prove the intermediate claim HGpreSub: Gpre ⊆ Fam.
An exact proof term for the current goal is (andEL (Gpre ⊆ Fam) (finite Gpre) HGpreLeft).
We prove the intermediate claim HGpreFin: finite Gpre.
An exact proof term for the current goal is (andER (Gpre ⊆ Fam) (finite Gpre) HGpreLeft).
We prove the intermediate claim HcovPrefA: (prefix a) ⊆ ⋃ Gpre.
An exact proof term for the current goal is (andER (Gpre ⊆ Fam ∧ finite Gpre) ((prefix a) ⊆ ⋃ Gpre) HGpre).
Set G to be the term Gpre ∪ {U0}.
We prove the intermediate claim HGFin: finite G.
An exact proof term for the current goal is (binunion_finite Gpre HGpreFin {U0} (Sing_finite U0)).
We prove the intermediate claim HGSub: G ⊆ Fam.
Let U be given.
Assume HU: U ∈ G.
Apply (binunionE Gpre {U0} U HU) to the current goal.
Assume HUGpre: U ∈ Gpre.
An exact proof term for the current goal is (HGpreSub U HUGpre).
Assume HUSing: U ∈ {U0}.
We prove the intermediate claim HUeq: U = U0.
An exact proof term for the current goal is (SingE U0 U HUSing).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is HU0Fam.
We prove the intermediate claim HcovPrefL: (prefix l) ⊆ ⋃ G.
Let x be given.
Assume Hx: x ∈ prefix l.
We will prove x ∈ ⋃ G.
We prove the intermediate claim HprefLdef: prefix l = {x0 ∈ unit_interval|Rle x0 l}.
Use reflexivity.
We prove the intermediate claim HxSep: x ∈ {x0 ∈ unit_interval|Rle x0 l}.
rewrite the current goal using HprefLdef (from right to left).
An exact proof term for the current goal is Hx.
We prove the intermediate claim HxI: x ∈ unit_interval.
An exact proof term for the current goal is (SepE1 unit_interval (λx0 : set ⇒ Rle x0 l) x HxSep).
We prove the intermediate claim HxleL: Rle x l.
An exact proof term for the current goal is (SepE2 unit_interval (λx0 : set ⇒ Rle x0 l) x HxSep).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R x HxI).
Apply (xm (Rlt a x) (x ∈ ⋃ G)) to the current goal.
Assume Hax: Rlt a x.
We prove the intermediate claim HcLtX: Rlt c x.
An exact proof term for the current goal is (Rlt_tra c a x HcLtA Hax).
We prove the intermediate claim HxLtd: Rlt x d.
An exact proof term for the current goal is (Rle_Rlt_tra x l d HxleL Hld).
We prove the intermediate claim HxInt: x ∈ open_interval c d.
We prove the intermediate claim HopenDef: open_interval c d = {z ∈ R|Rlt c z ∧ Rlt z d}.
Use reflexivity.
rewrite the current goal using HopenDef (from left to right).
Apply (SepI R (λz : set ⇒ Rlt c z ∧ Rlt z d) x HxR) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HcLtX.
An exact proof term for the current goal is HxLtd.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (HIntSubV x HxInt).
We prove the intermediate claim HxU0: x ∈ U0.
rewrite the current goal using HU0eq (from left to right).
An exact proof term for the current goal is (binintersectI V unit_interval x HxV HxI).
An exact proof term for the current goal is (UnionI G x U0 HxU0 (binunionI2 Gpre {U0} U0 (SingI U0))).
Assume Hnax: ¬ (Rlt a x).
We prove the intermediate claim HxleA: Rle x a.
An exact proof term for the current goal is (RleI x a HxR HaR Hnax).
We prove the intermediate claim HxPrefA: x ∈ prefix a.
We prove the intermediate claim HprefAdef: prefix a = {x0 ∈ unit_interval|Rle x0 a}.
Use reflexivity.
rewrite the current goal using HprefAdef (from left to right).
An exact proof term for the current goal is (SepI unit_interval (λx0 : set ⇒ Rle x0 a) x HxI HxleA).
We prove the intermediate claim HxUnionPre: x ∈ ⋃ Gpre.
An exact proof term for the current goal is (HcovPrefA x HxPrefA).
Apply (UnionE_impred Gpre x HxUnionPre (x ∈ ⋃ G)) to the current goal.
Let W be given.
Assume HxW: x ∈ W.
Assume HWGpre: W ∈ Gpre.
An exact proof term for the current goal is (UnionI G x W HxW (binunionI1 Gpre {U0} W HWGpre)).
We prove the intermediate claim HlGood: l ∈ Good.
We prove the intermediate claim HexL: ∃G0 : set, (G0 ⊆ Fam ∧ finite G0 ∧ (prefix l) ⊆ ⋃ G0).
We use G to witness the existential quantifier.
We will prove G ⊆ Fam ∧ finite G ∧ (prefix l) ⊆ ⋃ G.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HGSub.
An exact proof term for the current goal is HGFin.
An exact proof term for the current goal is HcovPrefL.
An exact proof term for the current goal is (SepI unit_interval (λa0 : set ⇒ ∃G0 : set, (G0 ⊆ Fam ∧ finite G0 ∧ (prefix a0) ⊆ ⋃ G0)) l HlI HexL).
Apply xm (Rlt 1 d) to the current goal.
Assume H1ltd: Rlt 1 d.
We prove the intermediate claim HcovPref1: (prefix 1) ⊆ ⋃ G.
Let x be given.
Assume Hx: x ∈ prefix 1.
We will prove x ∈ ⋃ G.
We prove the intermediate claim HxI: x ∈ unit_interval.
rewrite the current goal using Hprefix1 (from right to left).
An exact proof term for the current goal is Hx.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R x HxI).
We prove the intermediate claim Hxprop: ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x).
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) x HxI).
We prove the intermediate claim Hnlt1x: ¬ (Rlt 1 x).
An exact proof term for the current goal is (andER (¬ (Rlt x 0)) (¬ (Rlt 1 x)) Hxprop).
We prove the intermediate claim Hxle1: Rle x 1.
An exact proof term for the current goal is (RleI x 1 HxR real_1 Hnlt1x).
Apply (xm (Rlt l x) (x ∈ ⋃ G)) to the current goal.
Assume Hltlx: Rlt l x.
We prove the intermediate claim HcLtX: Rlt c x.
An exact proof term for the current goal is (Rlt_tra c l x Hcl Hltlx).
We prove the intermediate claim HxLtd: Rlt x d.
An exact proof term for the current goal is (Rle_Rlt_tra x 1 d Hxle1 H1ltd).
We prove the intermediate claim HxInt: x ∈ open_interval c d.
We prove the intermediate claim HopenDef: open_interval c d = {z ∈ R|Rlt c z ∧ Rlt z d}.
Use reflexivity.
rewrite the current goal using HopenDef (from left to right).
Apply (SepI R (λz : set ⇒ Rlt c z ∧ Rlt z d) x HxR) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HcLtX.
An exact proof term for the current goal is HxLtd.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (HIntSubV x HxInt).
We prove the intermediate claim HxU0: x ∈ U0.
rewrite the current goal using HU0eq (from left to right).
An exact proof term for the current goal is (binintersectI V unit_interval x HxV HxI).
An exact proof term for the current goal is (UnionI G x U0 HxU0 (binunionI2 Gpre {U0} U0 (SingI U0))).
Assume Hnltlx: ¬ (Rlt l x).
We prove the intermediate claim HxleL: Rle x l.
An exact proof term for the current goal is (RleI x l HxR HlR Hnltlx).
We prove the intermediate claim HxPrefL: x ∈ prefix l.
We prove the intermediate claim HprefLdef: prefix l = {x0 ∈ unit_interval|Rle x0 l}.
Use reflexivity.
rewrite the current goal using HprefLdef (from left to right).
An exact proof term for the current goal is (SepI unit_interval (λx0 : set ⇒ Rle x0 l) x HxI HxleL).
An exact proof term for the current goal is (HcovPrefL x HxPrefL).
We prove the intermediate claim HexG1: ∃G1 : set, (G1 ⊆ Fam ∧ finite G1 ∧ (prefix 1) ⊆ ⋃ G1).
We use G to witness the existential quantifier.
We will prove G ⊆ Fam ∧ finite G ∧ (prefix 1) ⊆ ⋃ G.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HGSub.
An exact proof term for the current goal is HGFin.
An exact proof term for the current goal is HcovPref1.
An exact proof term for the current goal is (SepI unit_interval (λa0 : set ⇒ ∃G0 : set, (G0 ⊆ Fam ∧ finite G0 ∧ (prefix a0) ⊆ ⋃ G0)) 1 one_in_unit_interval HexG1).
Assume Hn1ltd: ¬ (Rlt 1 d).
We will prove 1 ∈ Good.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim Hdle1: Rle d 1.
An exact proof term for the current goal is (RleI d 1 HdR real_1 Hn1ltd).
Set dgap to be the term add_SNo d (minus_SNo l).
We prove the intermediate claim HdgapR: dgap ∈ R.
An exact proof term for the current goal is (real_add_SNo d HdR (minus_SNo l) (real_minus_SNo l HlR)).
We prove the intermediate claim HdgapPos: Rlt 0 dgap.
An exact proof term for the current goal is (Rlt_0_diff_of_lt l d Hld).
We prove the intermediate claim HdgapS: SNo dgap.
An exact proof term for the current goal is (real_SNo dgap HdgapR).
We prove the intermediate claim HdgapPosS: 0 < dgap.
An exact proof term for the current goal is (RltE_lt 0 dgap HdgapPos).
Set delta to be the term mul_SNo (eps_ 1) dgap.
We prove the intermediate claim HdeltaR: delta ∈ R.
An exact proof term for the current goal is (real_mul_SNo (eps_ 1) eps_1_in_R dgap HdgapR).
We prove the intermediate claim HdeltaS: SNo delta.
An exact proof term for the current goal is (real_SNo delta HdeltaR).
We prove the intermediate claim HdeltaPosS: 0 < delta.
An exact proof term for the current goal is (mul_SNo_pos_pos (eps_ 1) dgap He1S HdgapS He1PosS HdgapPosS).
We prove the intermediate claim HdeltaPos: Rlt 0 delta.
An exact proof term for the current goal is (RltI 0 delta real_0 HdeltaR HdeltaPosS).
We prove the intermediate claim He1lt1: (eps_ 1) < 1.
An exact proof term for the current goal is (RltE_lt (eps_ 1) 1 eps_1_lt1_R).
We prove the intermediate claim HdeltaLtdgap: delta < dgap.
An exact proof term for the current goal is (mul_SNo_Lt1_pos_Lt (eps_ 1) dgap He1S HdgapS He1lt1 HdgapPosS).
Set b to be the term add_SNo l delta.
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (real_add_SNo l HlR delta HdeltaR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HlLtB: l < b.
rewrite the current goal using (add_SNo_0R l HlS) (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Lt2 l 0 delta HlS SNo_0 HdeltaS HdeltaPosS).
We prove the intermediate claim Hltlb: Rlt l b.
An exact proof term for the current goal is (RltI l b HlR HbR HlLtB).
We prove the intermediate claim HldgapEq: add_SNo l dgap = d.
We prove the intermediate claim HdS: SNo d.
An exact proof term for the current goal is (real_SNo d HdR).
We prove the intermediate claim Hassoc1: add_SNo l (add_SNo d (minus_SNo l)) = add_SNo (add_SNo l d) (minus_SNo l).
An exact proof term for the current goal is (add_SNo_assoc l d (minus_SNo l) HlS HdS (SNo_minus_SNo l HlS)).
We prove the intermediate claim Hcom1: add_SNo l d = add_SNo d l.
An exact proof term for the current goal is (add_SNo_com l d HlS HdS).
We prove the intermediate claim Hassoc2: add_SNo d (add_SNo l (minus_SNo l)) = add_SNo (add_SNo d l) (minus_SNo l).
An exact proof term for the current goal is (add_SNo_assoc d l (minus_SNo l) HdS HlS (SNo_minus_SNo l HlS)).
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using Hcom1 (from left to right).
rewrite the current goal using Hassoc2 (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv l HlS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R d HdS).
We prove the intermediate claim HbLtd: b < d.
We prove the intermediate claim Hstep: add_SNo l delta < add_SNo l dgap.
An exact proof term for the current goal is (add_SNo_Lt2 l delta dgap HlS HdeltaS HdgapS HdeltaLtdgap).
rewrite the current goal using HldgapEq (from right to left) at position 2.
An exact proof term for the current goal is Hstep.
We prove the intermediate claim Hltbd: Rlt b d.
An exact proof term for the current goal is (RltI b d HbR HdR HbLtd).
We prove the intermediate claim HbI: b ∈ unit_interval.
We prove the intermediate claim Hnltb0: ¬ (Rlt b 0).
Assume Hltb0: Rlt b 0.
We will prove False.
We prove the intermediate claim Hltl0: Rlt l 0.
An exact proof term for the current goal is (Rlt_tra l b 0 Hltlb Hltb0).
An exact proof term for the current goal is ((RleE_nlt 0 l Hl_ge0) Hltl0).
We prove the intermediate claim HbLe1: Rle b 1.
We prove the intermediate claim HbLed: Rle b d.
An exact proof term for the current goal is (Rlt_implies_Rle b d Hltbd).
An exact proof term for the current goal is (Rle_tra b d 1 HbLed Hdle1).
We prove the intermediate claim Hnlt1b: ¬ (Rlt 1 b).
An exact proof term for the current goal is (RleE_nlt b 1 HbLe1).
Apply (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) b HbR) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hnltb0.
An exact proof term for the current goal is Hnlt1b.
We prove the intermediate claim HbGood: b ∈ Good.
We prove the intermediate claim HcovPrefB: (prefix b) ⊆ ⋃ G.
Let x be given.
Assume Hx: x ∈ prefix b.
We will prove x ∈ ⋃ G.
We prove the intermediate claim HprefBdef: prefix b = {x0 ∈ unit_interval|Rle x0 b}.
Use reflexivity.
We prove the intermediate claim HxSep: x ∈ {x0 ∈ unit_interval|Rle x0 b}.
rewrite the current goal using HprefBdef (from right to left).
An exact proof term for the current goal is Hx.
We prove the intermediate claim HxI: x ∈ unit_interval.
An exact proof term for the current goal is (SepE1 unit_interval (λx0 : set ⇒ Rle x0 b) x HxSep).
We prove the intermediate claim HxleB: Rle x b.
An exact proof term for the current goal is (SepE2 unit_interval (λx0 : set ⇒ Rle x0 b) x HxSep).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R x HxI).
Apply (xm (Rlt l x) (x ∈ ⋃ G)) to the current goal.
Assume Hltlx: Rlt l x.
We prove the intermediate claim HcLtX: Rlt c x.
An exact proof term for the current goal is (Rlt_tra c l x Hcl Hltlx).
We prove the intermediate claim HxLtd': Rlt x d.
An exact proof term for the current goal is (Rle_Rlt_tra x b d HxleB Hltbd).
We prove the intermediate claim HxInt: x ∈ open_interval c d.
We prove the intermediate claim HopenDef: open_interval c d = {z ∈ R|Rlt c z ∧ Rlt z d}.
Use reflexivity.
rewrite the current goal using HopenDef (from left to right).
Apply (SepI R (λz : set ⇒ Rlt c z ∧ Rlt z d) x HxR) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HcLtX.
An exact proof term for the current goal is HxLtd'.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (HIntSubV x HxInt).
We prove the intermediate claim HxU0: x ∈ U0.
rewrite the current goal using HU0eq (from left to right).
An exact proof term for the current goal is (binintersectI V unit_interval x HxV HxI).
An exact proof term for the current goal is (UnionI G x U0 HxU0 (binunionI2 Gpre {U0} U0 (SingI U0))).
Assume Hnltlx: ¬ (Rlt l x).
We prove the intermediate claim HxleL: Rle x l.
An exact proof term for the current goal is (RleI x l HxR HlR Hnltlx).
We prove the intermediate claim HxPrefL: x ∈ prefix l.
We prove the intermediate claim HprefLdef: prefix l = {x0 ∈ unit_interval|Rle x0 l}.
Use reflexivity.
rewrite the current goal using HprefLdef (from left to right).
An exact proof term for the current goal is (SepI unit_interval (λx0 : set ⇒ Rle x0 l) x HxI HxleL).
An exact proof term for the current goal is (HcovPrefL x HxPrefL).
We prove the intermediate claim HexGb: ∃G0 : set, (G0 ⊆ Fam ∧ finite G0 ∧ (prefix b) ⊆ ⋃ G0).
We use G to witness the existential quantifier.
We will prove G ⊆ Fam ∧ finite G ∧ (prefix b) ⊆ ⋃ G.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HGSub.
An exact proof term for the current goal is HGFin.
An exact proof term for the current goal is HcovPrefB.
An exact proof term for the current goal is (SepI unit_interval (λa0 : set ⇒ ∃G0 : set, (G0 ⊆ Fam ∧ finite G0 ∧ (prefix a0) ⊆ ⋃ G0)) b HbI HexGb).
We prove the intermediate claim Hcore_lub: l ∈ R ∧ ∀a0 : set, a0 ∈ Good → a0 ∈ R → Rle a0 l.
An exact proof term for the current goal is (andEL (l ∈ R ∧ (∀a0 : set, a0 ∈ Good → a0 ∈ R → Rle a0 l)) (∀u : set, u ∈ R → (∀a0 : set, a0 ∈ Good → a0 ∈ R → Rle a0 u) → Rle l u) Hlub).
We prove the intermediate claim Hub: ∀a0 : set, a0 ∈ Good → a0 ∈ R → Rle a0 l.
An exact proof term for the current goal is (andER (l ∈ R) (∀a0 : set, a0 ∈ Good → a0 ∈ R → Rle a0 l) Hcore_lub).
We prove the intermediate claim HbleL: Rle b l.
An exact proof term for the current goal is (Hub b HbGood HbR).
An exact proof term for the current goal is ((RleE_nlt b l HbleL) Hltlb).
An exact proof term for the current goal is (Hfinish H1G).
∎