We will prove topology_on unit_interval unit_interval_topology ∧ ¬ (∃U V : set, U ∈ unit_interval_topology ∧ V ∈ unit_interval_topology ∧ separation_of unit_interval U V).
Apply andI to the current goal.
An exact proof term for the current goal is unit_interval_topology_on.
Assume Hsep: ∃U V : set, U ∈ unit_interval_topology ∧ V ∈ unit_interval_topology ∧ separation_of unit_interval U V.
Apply Hsep to the current goal.
Let U be given.
Assume HexV: ∃V : set, U ∈ unit_interval_topology ∧ V ∈ unit_interval_topology ∧ separation_of unit_interval U V.
Apply HexV to the current goal.
Let V be given.
Assume HUV: U ∈ unit_interval_topology ∧ V ∈ unit_interval_topology ∧ separation_of unit_interval U V.
We prove the intermediate claim HUV0: U ∈ unit_interval_topology ∧ V ∈ unit_interval_topology.
An exact proof term for the current goal is (andEL (U ∈ unit_interval_topology ∧ V ∈ unit_interval_topology) (separation_of unit_interval U V) HUV).
We prove the intermediate claim HUopen: U ∈ unit_interval_topology.
An exact proof term for the current goal is (andEL (U ∈ unit_interval_topology) (V ∈ unit_interval_topology) HUV0).
We prove the intermediate claim HVopen: V ∈ unit_interval_topology.
An exact proof term for the current goal is (andER (U ∈ unit_interval_topology) (V ∈ unit_interval_topology) HUV0).
We prove the intermediate claim HsepUV: separation_of unit_interval U V.
An exact proof term for the current goal is (andER (U ∈ unit_interval_topology ∧ V ∈ unit_interval_topology) (separation_of unit_interval U V) HUV).
We prove the intermediate claim Hpart1: ((((U ∈ 𝒫 unit_interval ∧ V ∈ 𝒫 unit_interval) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty).
An exact proof term for the current goal is (andEL ((((U ∈ 𝒫 unit_interval ∧ V ∈ 𝒫 unit_interval) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = unit_interval) HsepUV).
We prove the intermediate claim Hunion: U ∪ V = unit_interval.
An exact proof term for the current goal is (andER ((((U ∈ 𝒫 unit_interval ∧ V ∈ 𝒫 unit_interval) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = unit_interval) HsepUV).
We prove the intermediate claim HAux: (((U ∈ 𝒫 unit_interval ∧ V ∈ 𝒫 unit_interval) ∧ U ∩ V = Empty) ∧ U ≠ Empty).
An exact proof term for the current goal is (andEL (((U ∈ 𝒫 unit_interval ∧ V ∈ 𝒫 unit_interval) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) Hpart1).
We prove the intermediate claim HVne: V ≠ Empty.
An exact proof term for the current goal is (andER (((U ∈ 𝒫 unit_interval ∧ V ∈ 𝒫 unit_interval) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) Hpart1).
We prove the intermediate claim Hpowdisj: (U ∈ 𝒫 unit_interval ∧ V ∈ 𝒫 unit_interval) ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andEL ((U ∈ 𝒫 unit_interval ∧ V ∈ 𝒫 unit_interval) ∧ U ∩ V = Empty) (U ≠ Empty) HAux).
We prove the intermediate claim HUne: U ≠ Empty.
An exact proof term for the current goal is (andER ((U ∈ 𝒫 unit_interval ∧ V ∈ 𝒫 unit_interval) ∧ U ∩ V = Empty) (U ≠ Empty) HAux).
We prove the intermediate claim Hpow: U ∈ 𝒫 unit_interval ∧ V ∈ 𝒫 unit_interval.
An exact proof term for the current goal is (andEL (U ∈ 𝒫 unit_interval ∧ V ∈ 𝒫 unit_interval) (U ∩ V = Empty) Hpowdisj).
We prove the intermediate claim Hdisj: U ∩ V = Empty.
An exact proof term for the current goal is (andER (U ∈ 𝒫 unit_interval ∧ V ∈ 𝒫 unit_interval) (U ∩ V = Empty) Hpowdisj).
We prove the intermediate claim HUpow: U ∈ 𝒫 unit_interval.
An exact proof term for the current goal is (andEL (U ∈ 𝒫 unit_interval) (V ∈ 𝒫 unit_interval) Hpow).
We prove the intermediate claim HVpow: V ∈ 𝒫 unit_interval.
An exact proof term for the current goal is (andER (U ∈ 𝒫 unit_interval) (V ∈ 𝒫 unit_interval) Hpow).
We prove the intermediate claim HUsub: U ⊆ unit_interval.
An exact proof term for the current goal is (PowerE unit_interval U HUpow).
We prove the intermediate claim HVsub: V ⊆ unit_interval.
An exact proof term for the current goal is (PowerE unit_interval V HVpow).
We prove the intermediate claim Hexu0: ∃u0 : set, u0 ∈ U.
An exact proof term for the current goal is (nonempty_has_element U HUne).
We prove the intermediate claim Hexv0: ∃v0 : set, v0 ∈ V.
An exact proof term for the current goal is (nonempty_has_element V HVne).
Apply Hexu0 to the current goal.
Let u0 be given.
Assume Hu0U: u0 ∈ U.
Apply Hexv0 to the current goal.
Let v0 be given.
Assume Hv0V: v0 ∈ V.
We prove the intermediate claim Hu0I: u0 ∈ unit_interval.
An exact proof term for the current goal is (HUsub u0 Hu0U).
We prove the intermediate claim Hv0I: v0 ∈ unit_interval.
An exact proof term for the current goal is (HVsub v0 Hv0V).
We prove the intermediate claim Hu0R: u0 ∈ R.
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) u0 Hu0I).
We prove the intermediate claim Hv0R: v0 ∈ R.
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) v0 Hv0I).
We prove the intermediate claim Hu0S: SNo u0.
An exact proof term for the current goal is (real_SNo u0 Hu0R).
We prove the intermediate claim Hv0S: SNo v0.
An exact proof term for the current goal is (real_SNo v0 Hv0R).
We will prove False.
Apply (SNoLt_trichotomy_or_impred u0 v0 Hu0S Hv0S False) to the current goal.
Assume Hu0ltv0: u0 < v0.
Set A to be the term {u ∈ U|Rlt u v0}.
We prove the intermediate claim Hu0Rltv0: Rlt u0 v0.
An exact proof term for the current goal is (RltI u0 v0 Hu0R Hv0R Hu0ltv0).
We prove the intermediate claim Hu0inA: u0 ∈ A.
An exact proof term for the current goal is (SepI U (λu : set ⇒ Rlt u v0) u0 Hu0U Hu0Rltv0).
We prove the intermediate claim HAinR: ∀a : set, a ∈ A → a ∈ R.
Let a be given.
Assume HaA: a ∈ A.
We prove the intermediate claim HaU: a ∈ U.
An exact proof term for the current goal is (SepE1 U (λu : set ⇒ Rlt u v0) a HaA).
We prove the intermediate claim HaI: a ∈ unit_interval.
An exact proof term for the current goal is (HUsub a HaU).
An exact proof term for the current goal is (unit_interval_sub_R a HaI).
We prove the intermediate claim Hub_ex: ∃u : set, u ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a u.
We use v0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv0R.
Let a be given.
Assume HaA: a ∈ A.
Assume _.
We prove the intermediate claim Harlt: Rlt a v0.
An exact proof term for the current goal is (SepE2 U (λu : set ⇒ Rlt u v0) a HaA).
An exact proof term for the current goal is (Rlt_implies_Rle a v0 Harlt).
We prove the intermediate claim HAnen: ∃a0 : set, a0 ∈ A.
We use u0 to witness the existential quantifier.
An exact proof term for the current goal is Hu0inA.
We prove the intermediate claim Hexlub: ∃l : set, R_lub A l.
An exact proof term for the current goal is (R_lub_exists A HAnen HAinR Hub_ex).
Apply Hexlub to the current goal.
Let l be given.
Assume Hlub: R_lub A l.
We prove the intermediate claim HlR: l ∈ R.
An exact proof term for the current goal is (R_lub_in_R A l Hlub).
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 Hlubcore: l ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l.
An exact proof term for the current goal is (andEL (l ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l) (∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l u) Hlub).
We prove the intermediate claim HubA: ∀a : set, a ∈ A → a ∈ R → Rle a l.
An exact proof term for the current goal is (andER (l ∈ R) (∀a : set, a ∈ A → a ∈ R → Rle a l) Hlubcore).
We prove the intermediate claim Hmin: ∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l u.
An exact proof term for the current goal is (andER (l ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l) (∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l u) Hlub).
We prove the intermediate claim Hlubv0: Rle l v0.
Apply (Hmin v0 Hv0R) to the current goal.
Let a be given.
Assume HaA: a ∈ A.
Assume _.
We prove the intermediate claim Harlt: Rlt a v0.
An exact proof term for the current goal is (SepE2 U (λu : set ⇒ Rlt u v0) a HaA).
An exact proof term for the current goal is (Rlt_implies_Rle a v0 Harlt).
We prove the intermediate claim Hu0conj: ¬ (Rlt u0 0) ∧ ¬ (Rlt 1 u0).
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) u0 Hu0I).
We prove the intermediate claim Hnlt_u0_0: ¬ (Rlt u0 0).
An exact proof term for the current goal is (andEL (¬ (Rlt u0 0)) (¬ (Rlt 1 u0)) Hu0conj).
We prove the intermediate claim Hu0ge0: Rle 0 u0.
An exact proof term for the current goal is (RleI 0 u0 real_0 Hu0R Hnlt_u0_0).
We prove the intermediate claim Hu0le_l: Rle u0 l.
An exact proof term for the current goal is (HubA u0 Hu0inA Hu0R).
We prove the intermediate claim H0le_l: Rle 0 l.
An exact proof term for the current goal is (Rle_tra 0 u0 l Hu0ge0 Hu0le_l).
We prove the intermediate claim H1R: 1 ∈ R.
An exact proof term for the current goal is real_1.
We prove the intermediate claim Hlub1: Rle l 1.
Apply (Hmin 1 H1R) to the current goal.
Let a be given.
Assume HaA: a ∈ A.
Assume HaR: a ∈ R.
We prove the intermediate claim HaU: a ∈ U.
An exact proof term for the current goal is (SepE1 U (λu : set ⇒ Rlt u v0) a HaA).
We prove the intermediate claim HaI: a ∈ unit_interval.
An exact proof term for the current goal is (HUsub a HaU).
We prove the intermediate claim Haconj: ¬ (Rlt a 0) ∧ ¬ (Rlt 1 a).
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) a (HUsub a HaU)).
We prove the intermediate claim Hnlt_1a: ¬ (Rlt 1 a).
An exact proof term for the current goal is (andER (¬ (Rlt a 0)) (¬ (Rlt 1 a)) Haconj).
An exact proof term for the current goal is (RleI a 1 HaR H1R Hnlt_1a).
We prove the intermediate claim Hnlt_l_0: ¬ (Rlt l 0).
An exact proof term for the current goal is (RleE_nlt 0 l H0le_l).
We prove the intermediate claim Hnlt_1_l: ¬ (Rlt 1 l).
An exact proof term for the current goal is (RleE_nlt l 1 Hlub1).
We prove the intermediate claim HlI: l ∈ unit_interval.
An exact proof term for the current goal is (SepI R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) l HlR (andI (¬ (Rlt l 0)) (¬ (Rlt 1 l)) Hnlt_l_0 Hnlt_1_l)).
We prove the intermediate claim HlUV: l ∈ U ∪ V.
rewrite the current goal using Hunion (from left to right).
An exact proof term for the current goal is HlI.
Apply (binunionE U V l HlUV) to the current goal.
Assume HlU: l ∈ U.
We prove the intermediate claim Hv0notU: v0 ∉ U.
Assume Hv0U: v0 ∈ U.
We prove the intermediate claim Hv0UV: v0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V v0 Hv0U Hv0V).
We prove the intermediate claim Hv0Empty: v0 ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is Hv0UV.
An exact proof term for the current goal is (EmptyE v0 Hv0Empty).
We prove the intermediate claim HUopen_in: open_in unit_interval unit_interval_topology U.
An exact proof term for the current goal is (open_inI unit_interval unit_interval_topology U unit_interval_topology_on HUopen).
We prove the intermediate claim HexUamb: ∃Uamb ∈ R_standard_topology, U = Uamb ∩ unit_interval.
An exact proof term for the current goal is (iffEL (open_in unit_interval unit_interval_topology U) (∃Uamb ∈ R_standard_topology, U = Uamb ∩ unit_interval) (open_in_subspace_iff R R_standard_topology unit_interval U R_standard_topology_is_topology unit_interval_sub_R HUsub) HUopen_in).
Apply HexUamb to the current goal.
Let Uamb be given.
Assume HUambpair: Uamb ∈ R_standard_topology ∧ U = Uamb ∩ unit_interval.
We prove the intermediate claim HUambOpen: Uamb ∈ R_standard_topology.
An exact proof term for the current goal is (andEL (Uamb ∈ R_standard_topology) (U = Uamb ∩ unit_interval) HUambpair).
We prove the intermediate claim HUeq: U = Uamb ∩ unit_interval.
An exact proof term for the current goal is (andER (Uamb ∈ R_standard_topology) (U = Uamb ∩ unit_interval) HUambpair).
We prove the intermediate claim HlUamb: l ∈ Uamb.
We prove the intermediate claim HlU2: l ∈ Uamb ∩ unit_interval.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HlU.
An exact proof term for the current goal is (binintersectE1 Uamb unit_interval l HlU2).
We prove the intermediate claim Hexcd: ∃c d : set, c ∈ R ∧ d ∈ R ∧ l ∈ open_interval c d ∧ open_interval c d ⊆ Uamb ∧ Rlt c l ∧ Rlt l d.
An exact proof term for the current goal is (R_standard_open_refine_interval Uamb l HUambOpen HlUamb).
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 ⊆ Uamb) ∧ 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 ⊆ Uamb) ∧ 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 ⊆ Uamb) ∧ 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 ⊆ Uamb).
An exact proof term for the current goal is (andEL (((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) ∧ open_interval c d ⊆ Uamb) (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 ⊆ Uamb) (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 ⊆ Uamb) Hcd2).
We prove the intermediate claim HIntSubUamb: open_interval c d ⊆ Uamb.
An exact proof term for the current goal is (andER ((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) (open_interval c d ⊆ Uamb) Hcd2).
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (andEL (c ∈ R) (d ∈ R) (andEL (c ∈ R ∧ d ∈ R) (l ∈ open_interval c d) Hcd3)).
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (andER (c ∈ R) (d ∈ R) (andEL (c ∈ R ∧ d ∈ R) (l ∈ open_interval c d) Hcd3)).
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 Hlneqv0: ¬ (l = v0).
Assume Heq: l = v0.
We prove the intermediate claim Hv0U': v0 ∈ U.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HlU.
An exact proof term for the current goal is (Hv0notU Hv0U').
We prove the intermediate claim Hlv0: Rlt l v0.
Apply (SNoLt_trichotomy_or_impred l v0 HlS Hv0S (Rlt l v0)) to the current goal.
Assume Hlt: l < v0.
An exact proof term for the current goal is (RltI l v0 HlR Hv0R Hlt).
Assume Heq: l = v0.
An exact proof term for the current goal is (FalseE (Hlneqv0 Heq) (Rlt l v0)).
Assume Hgt: v0 < l.
We prove the intermediate claim Hv0l: Rlt v0 l.
An exact proof term for the current goal is (RltI v0 l Hv0R HlR Hgt).
We prove the intermediate claim Hnlt: ¬ (Rlt v0 l).
An exact proof term for the current goal is (RleE_nlt l v0 Hlubv0).
An exact proof term for the current goal is (FalseE (Hnlt Hv0l) (Rlt l v0)).
Set gap1 to be the term add_SNo d (minus_SNo l).
Set gap2 to be the term add_SNo v0 (minus_SNo l).
We prove the intermediate claim Hgap1R: gap1 ∈ 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 Hgap2R: gap2 ∈ R.
An exact proof term for the current goal is (real_add_SNo v0 Hv0R (minus_SNo l) (real_minus_SNo l HlR)).
We prove the intermediate claim Hgap1pos: Rlt 0 gap1.
An exact proof term for the current goal is (Rlt_0_diff_of_lt l d Hld).
We prove the intermediate claim Hgap2pos: Rlt 0 gap2.
An exact proof term for the current goal is (Rlt_0_diff_of_lt l v0 Hlv0).
Apply (exists_eps_lt_two_pos_Euclid gap1 gap2 Hgap1R Hgap2R Hgap1pos Hgap2pos) to the current goal.
Let r3 be given.
Assume Hr3pack.
We prove the intermediate claim Hr3p1: (r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 gap1.
An exact proof term for the current goal is (andEL ((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 gap1) (Rlt r3 gap2) Hr3pack).
We prove the intermediate claim Hr3ltgap2: Rlt r3 gap2.
An exact proof term for the current goal is (andER ((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 gap1) (Rlt r3 gap2) Hr3pack).
We prove the intermediate claim Hr3p0: r3 ∈ R ∧ Rlt 0 r3.
An exact proof term for the current goal is (andEL (r3 ∈ R ∧ Rlt 0 r3) (Rlt r3 gap1) Hr3p1).
We prove the intermediate claim Hr3ltgap1: Rlt r3 gap1.
An exact proof term for the current goal is (andER (r3 ∈ R ∧ Rlt 0 r3) (Rlt r3 gap1) Hr3p1).
We prove the intermediate claim Hr3R: r3 ∈ R.
An exact proof term for the current goal is (andEL (r3 ∈ R) (Rlt 0 r3) Hr3p0).
We prove the intermediate claim Hr3pos: Rlt 0 r3.
An exact proof term for the current goal is (andER (r3 ∈ R) (Rlt 0 r3) Hr3p0).
We prove the intermediate claim Hr3S: SNo r3.
An exact proof term for the current goal is (real_SNo r3 Hr3R).
We prove the intermediate claim Hr3posS: 0 < r3.
An exact proof term for the current goal is (RltE_lt 0 r3 Hr3pos).
We prove the intermediate claim Hu1R: add_SNo l r3 ∈ R.
An exact proof term for the current goal is (real_add_SNo l HlR r3 Hr3R).
We prove the intermediate claim Hu1S: SNo (add_SNo l r3).
An exact proof term for the current goal is (real_SNo (add_SNo l r3) Hu1R).
We prove the intermediate claim Hl_lt_u1S: l < add_SNo l r3.
We prove the intermediate claim Hl0: add_SNo l 0 = l.
An exact proof term for the current goal is (add_SNo_0R l HlS).
We prove the intermediate claim Hlt: add_SNo l 0 < add_SNo l r3.
An exact proof term for the current goal is (add_SNo_Lt2 l 0 r3 HlS SNo_0 Hr3S Hr3posS).
rewrite the current goal using Hl0 (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Hl_lt_u1: Rlt l (add_SNo l r3).
An exact proof term for the current goal is (RltI l (add_SNo l r3) HlR Hu1R Hl_lt_u1S).
We prove the intermediate claim Hr3ltgap1S: r3 < gap1.
An exact proof term for the current goal is (RltE_lt r3 gap1 Hr3ltgap1).
We prove the intermediate claim Hgap1S: SNo gap1.
An exact proof term for the current goal is (real_SNo gap1 Hgap1R).
We prove the intermediate claim Hu1lt_dS': add_SNo r3 l < d.
An exact proof term for the current goal is (add_SNo_minus_Lt2 d l r3 HdS HlS Hr3S Hr3ltgap1S).
We prove the intermediate claim Hu1lt_dS: add_SNo l r3 < d.
We prove the intermediate claim Hcom2: add_SNo r3 l = add_SNo l r3.
An exact proof term for the current goal is (add_SNo_com r3 l Hr3S HlS).
rewrite the current goal using Hcom2 (from right to left).
An exact proof term for the current goal is Hu1lt_dS'.
We prove the intermediate claim Hu1lt_d: Rlt (add_SNo l r3) d.
An exact proof term for the current goal is (RltI (add_SNo l r3) d Hu1R HdR Hu1lt_dS).
We prove the intermediate claim Hr3ltgap2S: r3 < gap2.
An exact proof term for the current goal is (RltE_lt r3 gap2 Hr3ltgap2).
We prove the intermediate claim Hgap2S: SNo gap2.
An exact proof term for the current goal is (real_SNo gap2 Hgap2R).
We prove the intermediate claim Hu1lt_v0S': add_SNo r3 l < v0.
An exact proof term for the current goal is (add_SNo_minus_Lt2 v0 l r3 Hv0S HlS Hr3S Hr3ltgap2S).
We prove the intermediate claim Hu1lt_v0S: add_SNo l r3 < v0.
We prove the intermediate claim Hcom3: add_SNo r3 l = add_SNo l r3.
An exact proof term for the current goal is (add_SNo_com r3 l Hr3S HlS).
rewrite the current goal using Hcom3 (from right to left).
An exact proof term for the current goal is Hu1lt_v0S'.
We prove the intermediate claim Hu1lt_v0: Rlt (add_SNo l r3) v0.
An exact proof term for the current goal is (RltI (add_SNo l r3) v0 Hu1R Hv0R Hu1lt_v0S).
We prove the intermediate claim Hu1InInt: add_SNo l r3 ∈ open_interval c d.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt c z ∧ Rlt z d) (add_SNo l r3) Hu1R (andI (Rlt c (add_SNo l r3)) (Rlt (add_SNo l r3) d) (Rlt_tra c l (add_SNo l r3) Hcl Hl_lt_u1) Hu1lt_d)).
We prove the intermediate claim Hu1Uamb: add_SNo l r3 ∈ Uamb.
An exact proof term for the current goal is (HIntSubUamb (add_SNo l r3) Hu1InInt).
We prove the intermediate claim Hv0conj: ¬ (Rlt v0 0) ∧ ¬ (Rlt 1 v0).
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) v0 Hv0I).
We prove the intermediate claim Hnlt_1v0: ¬ (Rlt 1 v0).
An exact proof term for the current goal is (andER (¬ (Rlt v0 0)) (¬ (Rlt 1 v0)) Hv0conj).
We prove the intermediate claim Hv0le1: Rle v0 1.
An exact proof term for the current goal is (RleI v0 1 Hv0R H1R Hnlt_1v0).
We prove the intermediate claim Hu1le_v0: Rle (add_SNo l r3) v0.
An exact proof term for the current goal is (Rlt_implies_Rle (add_SNo l r3) v0 Hu1lt_v0).
We prove the intermediate claim Hu1le1: Rle (add_SNo l r3) 1.
An exact proof term for the current goal is (Rle_tra (add_SNo l r3) v0 1 Hu1le_v0 Hv0le1).
We prove the intermediate claim Hl_le_u1: Rle l (add_SNo l r3).
An exact proof term for the current goal is (Rlt_implies_Rle l (add_SNo l r3) Hl_lt_u1).
We prove the intermediate claim H0le_u1: Rle 0 (add_SNo l r3).
An exact proof term for the current goal is (Rle_tra 0 l (add_SNo l r3) H0le_l Hl_le_u1).
We prove the intermediate claim Hnlt_u1_0: ¬ (Rlt (add_SNo l r3) 0).
An exact proof term for the current goal is (RleE_nlt 0 (add_SNo l r3) H0le_u1).
We prove the intermediate claim Hnlt_1_u1: ¬ (Rlt 1 (add_SNo l r3)).
An exact proof term for the current goal is (RleE_nlt (add_SNo l r3) 1 Hu1le1).
We prove the intermediate claim Hu1I: add_SNo l r3 ∈ unit_interval.
An exact proof term for the current goal is (SepI R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) (add_SNo l r3) Hu1R (andI (¬ (Rlt (add_SNo l r3) 0)) (¬ (Rlt 1 (add_SNo l r3))) Hnlt_u1_0 Hnlt_1_u1)).
We prove the intermediate claim Hu1U: add_SNo l r3 ∈ U.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (binintersectI Uamb unit_interval (add_SNo l r3) Hu1Uamb Hu1I).
We prove the intermediate claim Hu1A: add_SNo l r3 ∈ A.
An exact proof term for the current goal is (SepI U (λu : set ⇒ Rlt u v0) (add_SNo l r3) Hu1U Hu1lt_v0).
We prove the intermediate claim Hu1le_l: Rle (add_SNo l r3) l.
An exact proof term for the current goal is (HubA (add_SNo l r3) Hu1A Hu1R).
We prove the intermediate claim Hnlt: ¬ (Rlt l (add_SNo l r3)).
An exact proof term for the current goal is (RleE_nlt (add_SNo l r3) l Hu1le_l).
An exact proof term for the current goal is (Hnlt Hl_lt_u1).
Assume HlV: l ∈ V.
We prove the intermediate claim HVopen_in: open_in unit_interval unit_interval_topology V.
An exact proof term for the current goal is (open_inI unit_interval unit_interval_topology V unit_interval_topology_on HVopen).
We prove the intermediate claim HexVamb: ∃Vamb ∈ R_standard_topology, V = Vamb ∩ unit_interval.
An exact proof term for the current goal is (iffEL (open_in unit_interval unit_interval_topology V) (∃Vamb ∈ R_standard_topology, V = Vamb ∩ unit_interval) (open_in_subspace_iff R R_standard_topology unit_interval V R_standard_topology_is_topology unit_interval_sub_R HVsub) HVopen_in).
Apply HexVamb to the current goal.
Let Vamb be given.
Assume HVambpair: Vamb ∈ R_standard_topology ∧ V = Vamb ∩ unit_interval.
We prove the intermediate claim HVambOpen: Vamb ∈ R_standard_topology.
An exact proof term for the current goal is (andEL (Vamb ∈ R_standard_topology) (V = Vamb ∩ unit_interval) HVambpair).
We prove the intermediate claim HVeq: V = Vamb ∩ unit_interval.
An exact proof term for the current goal is (andER (Vamb ∈ R_standard_topology) (V = Vamb ∩ unit_interval) HVambpair).
We prove the intermediate claim HlVamb: l ∈ Vamb.
We prove the intermediate claim HlV2: l ∈ Vamb ∩ unit_interval.
rewrite the current goal using HVeq (from right to left).
An exact proof term for the current goal is HlV.
An exact proof term for the current goal is (binintersectE1 Vamb unit_interval l HlV2).
We prove the intermediate claim Hexcd: ∃c d : set, c ∈ R ∧ d ∈ R ∧ l ∈ open_interval c d ∧ open_interval c d ⊆ Vamb ∧ Rlt c l ∧ Rlt l d.
An exact proof term for the current goal is (R_standard_open_refine_interval Vamb l HVambOpen HlVamb).
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 ⊆ Vamb) ∧ 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 ⊆ Vamb) ∧ 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 ⊆ Vamb) ∧ 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 ⊆ Vamb).
An exact proof term for the current goal is (andEL (((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) ∧ open_interval c d ⊆ Vamb) (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 ⊆ Vamb) (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 ⊆ Vamb) Hcd2).
We prove the intermediate claim HIntSubVamb: open_interval c d ⊆ Vamb.
An exact proof term for the current goal is (andER ((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) (open_interval c d ⊆ Vamb) Hcd2).
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (andEL (c ∈ R) (d ∈ R) (andEL (c ∈ R ∧ d ∈ R) (l ∈ open_interval c d) Hcd3)).
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (andER (c ∈ R) (d ∈ R) (andEL (c ∈ R ∧ d ∈ R) (l ∈ open_interval c d) Hcd3)).
We prove the intermediate claim HlS2: SNo l.
An exact proof term for the current goal is HlS.
We prove the intermediate claim HdS: SNo d.
An exact proof term for the current goal is (real_SNo d HdR).
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 Hexeps: ∃Neps ∈ ω, eps_ Neps < gap.
An exact proof term for the current goal is (exists_eps_lt_pos_Euclid gap HgapR HgapPos).
Apply Hexeps to the current goal.
Let Neps be given.
Assume HNepspair.
We prove the intermediate claim HNepsO: Neps ∈ ω.
An exact proof term for the current goal is (andEL (Neps ∈ ω) (eps_ Neps < gap) HNepspair).
We prove the intermediate claim HepsltS: eps_ Neps < gap.
An exact proof term for the current goal is (andER (Neps ∈ ω) (eps_ Neps < gap) HNepspair).
We prove the intermediate claim HepsR: eps_ Neps ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ Neps) (SNo_eps_SNoS_omega Neps HNepsO)).
We prove the intermediate claim HepsposS: 0 < eps_ Neps.
An exact proof term for the current goal is (SNo_eps_pos Neps HNepsO).
We prove the intermediate claim Hepspos: Rlt 0 (eps_ Neps).
An exact proof term for the current goal is (RltI 0 (eps_ Neps) real_0 HepsR HepsposS).
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 HepsS: SNo (eps_ Neps).
An exact proof term for the current goal is (real_SNo (eps_ Neps) HepsR).
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 HepsltR: Rlt (eps_ Neps) gap.
An exact proof term for the current goal is (RltI (eps_ Neps) gap HepsR HgapR HepsltS).
We prove the intermediate claim HepsltgapS: eps_ Neps < gap.
An exact proof term for the current goal is (RltE_lt (eps_ Neps) gap HepsltR).
We prove the intermediate claim Hsumlt1: add_SNo (eps_ Neps) c < l.
An exact proof term for the current goal is (add_SNo_minus_Lt2 l c (eps_ Neps) HlS2 HcS HepsS HepsltgapS).
We prove the intermediate claim Hsumlt2: add_SNo c (eps_ Neps) < l.
rewrite the current goal using (add_SNo_com c (eps_ Neps) HcS HepsS) (from left to right).
An exact proof term for the current goal is Hsumlt1.
We prove the intermediate claim Hclm: c < add_SNo l (minus_SNo (eps_ Neps)).
An exact proof term for the current goal is (add_SNo_minus_Lt2b l (eps_ Neps) c HlS2 HepsS HcS Hsumlt2).
We prove the intermediate claim HclmR: add_SNo l (minus_SNo (eps_ Neps)) ∈ R.
An exact proof term for the current goal is (real_add_SNo l HlR (minus_SNo (eps_ Neps)) (real_minus_SNo (eps_ Neps) HepsR)).
We prove the intermediate claim HclmRlt: Rlt c (add_SNo l (minus_SNo (eps_ Neps))).
An exact proof term for the current goal is (RltI c (add_SNo l (minus_SNo (eps_ Neps))) HcR HclmR Hclm).
We prove the intermediate claim Hexa: ∃a : set, a ∈ A ∧ a ∈ R ∧ Rlt (add_SNo l (minus_SNo (eps_ Neps))) a.
An exact proof term for the current goal is (R_lub_approx_from_below A l (eps_ Neps) Hlub HepsR Hepspos).
Apply Hexa to the current goal.
Let a be given.
Assume Haa.
We prove the intermediate claim Haa1: a ∈ A ∧ a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ A ∧ a ∈ R) (Rlt (add_SNo l (minus_SNo (eps_ Neps))) a) Haa).
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (andEL (a ∈ A) (a ∈ R) Haa1).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andER (a ∈ A) (a ∈ R) Haa1).
We prove the intermediate claim Hltlm: Rlt (add_SNo l (minus_SNo (eps_ Neps))) a.
An exact proof term for the current goal is (andER (a ∈ A ∧ a ∈ R) (Rlt (add_SNo l (minus_SNo (eps_ Neps))) a) Haa).
We prove the intermediate claim Hcalt: c < a.
An exact proof term for the current goal is (RltE_lt c a (Rlt_tra c (add_SNo l (minus_SNo (eps_ Neps))) a HclmRlt Hltlm)).
We prove the intermediate claim Hca: Rlt c a.
An exact proof term for the current goal is (RltI c a HcR HaR Hcalt).
We prove the intermediate claim HubA2: ∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 l.
An exact proof term for the current goal is (andER (l ∈ R) (∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 l) Hlubcore).
We prove the intermediate claim Hale_l: Rle a l.
An exact proof term for the current goal is (HubA2 a HaA HaR).
We prove the intermediate claim Hnltla: ¬ (Rlt l a).
An exact proof term for the current goal is (RleE_nlt a l Hale_l).
We prove the intermediate claim Had: Rlt a d.
Apply (SNoLt_trichotomy_or_impred a l (real_SNo a HaR) HlS2 (Rlt a d)) to the current goal.
Assume Haltl: a < l.
We prove the intermediate claim HaltlR: Rlt a l.
An exact proof term for the current goal is (RltI a l HaR HlR Haltl).
An exact proof term for the current goal is (Rlt_tra a l d HaltlR Hld).
Assume Haeq: a = l.
rewrite the current goal using Haeq (from left to right).
An exact proof term for the current goal is Hld.
Assume Hlta: l < a.
We prove the intermediate claim HltaR: Rlt l a.
An exact proof term for the current goal is (RltI l a HlR HaR Hlta).
An exact proof term for the current goal is (FalseE (Hnltla HltaR) (Rlt a d)).
We prove the intermediate claim HaInInt: a ∈ open_interval c d.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt c z ∧ Rlt z d) a HaR (andI (Rlt c a) (Rlt a d) Hca Had)).
We prove the intermediate claim HaVamb: a ∈ Vamb.
An exact proof term for the current goal is (HIntSubVamb a HaInInt).
We prove the intermediate claim HaU: a ∈ U.
An exact proof term for the current goal is (SepE1 U (λu : set ⇒ Rlt u v0) a HaA).
We prove the intermediate claim HaI: a ∈ unit_interval.
An exact proof term for the current goal is (HUsub a HaU).
We prove the intermediate claim HaV: a ∈ V.
rewrite the current goal using HVeq (from left to right).
An exact proof term for the current goal is (binintersectI Vamb unit_interval a HaVamb HaI).
We prove the intermediate claim HaUV: a ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V a HaU HaV).
We prove the intermediate claim HaEmpty: a ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HaUV.
An exact proof term for the current goal is (EmptyE a HaEmpty).
Assume Heq: u0 = v0.
We prove the intermediate claim Hu0V: u0 ∈ V.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hv0V.
We prove the intermediate claim Hu0UV: u0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V u0 Hu0U Hu0V).
We prove the intermediate claim Hu0E: u0 ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is Hu0UV.
An exact proof term for the current goal is (EmptyE u0 Hu0E).
Assume Hv0ltu0: v0 < u0.
Set A to be the term {v ∈ V|Rlt v u0}.
We prove the intermediate claim Hv0Rltu0: Rlt v0 u0.
An exact proof term for the current goal is (RltI v0 u0 Hv0R Hu0R Hv0ltu0).
We prove the intermediate claim Hv0inA: v0 ∈ A.
An exact proof term for the current goal is (SepI V (λv : set ⇒ Rlt v u0) v0 Hv0V Hv0Rltu0).
We prove the intermediate claim HAinR: ∀a : set, a ∈ A → a ∈ R.
Let a be given.
Assume HaA: a ∈ A.
We prove the intermediate claim HaV: a ∈ V.
An exact proof term for the current goal is (SepE1 V (λv : set ⇒ Rlt v u0) a HaA).
We prove the intermediate claim HaI: a ∈ unit_interval.
An exact proof term for the current goal is (HVsub a HaV).
An exact proof term for the current goal is (unit_interval_sub_R a HaI).
We prove the intermediate claim Hub_ex: ∃u : set, u ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a u.
We use u0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hu0R.
Let a be given.
Assume HaA: a ∈ A.
Assume _.
We prove the intermediate claim Harlt: Rlt a u0.
An exact proof term for the current goal is (SepE2 V (λv : set ⇒ Rlt v u0) a HaA).
An exact proof term for the current goal is (Rlt_implies_Rle a u0 Harlt).
We prove the intermediate claim HAnen: ∃a0 : set, a0 ∈ A.
We use v0 to witness the existential quantifier.
An exact proof term for the current goal is Hv0inA.
We prove the intermediate claim Hexlub: ∃l : set, R_lub A l.
An exact proof term for the current goal is (R_lub_exists A HAnen HAinR Hub_ex).
Apply Hexlub to the current goal.
Let l be given.
Assume Hlub: R_lub A l.
We prove the intermediate claim HlR: l ∈ R.
An exact proof term for the current goal is (R_lub_in_R A l Hlub).
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 Hlubcore: l ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l.
An exact proof term for the current goal is (andEL (l ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l) (∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l u) Hlub).
We prove the intermediate claim HubA: ∀a : set, a ∈ A → a ∈ R → Rle a l.
An exact proof term for the current goal is (andER (l ∈ R) (∀a : set, a ∈ A → a ∈ R → Rle a l) Hlubcore).
We prove the intermediate claim Hmin: ∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l u.
An exact proof term for the current goal is (andER (l ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l) (∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l u) Hlub).
We prove the intermediate claim Hlubu0: Rle l u0.
Apply (Hmin u0 Hu0R) to the current goal.
Let a be given.
Assume HaA: a ∈ A.
Assume _.
We prove the intermediate claim Harlt: Rlt a u0.
An exact proof term for the current goal is (SepE2 V (λv : set ⇒ Rlt v u0) a HaA).
An exact proof term for the current goal is (Rlt_implies_Rle a u0 Harlt).
We prove the intermediate claim Hv0conj: ¬ (Rlt v0 0) ∧ ¬ (Rlt 1 v0).
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) v0 Hv0I).
We prove the intermediate claim Hnlt_v0_0: ¬ (Rlt v0 0).
An exact proof term for the current goal is (andEL (¬ (Rlt v0 0)) (¬ (Rlt 1 v0)) Hv0conj).
We prove the intermediate claim Hv0ge0: Rle 0 v0.
An exact proof term for the current goal is (RleI 0 v0 real_0 Hv0R Hnlt_v0_0).
We prove the intermediate claim Hv0le_l: Rle v0 l.
An exact proof term for the current goal is (HubA v0 Hv0inA Hv0R).
We prove the intermediate claim H0le_l: Rle 0 l.
An exact proof term for the current goal is (Rle_tra 0 v0 l Hv0ge0 Hv0le_l).
We prove the intermediate claim H1R: 1 ∈ R.
An exact proof term for the current goal is real_1.
We prove the intermediate claim Hlub1: Rle l 1.
Apply (Hmin 1 H1R) to the current goal.
Let a be given.
Assume HaA: a ∈ A.
Assume HaR: a ∈ R.
We prove the intermediate claim HaV: a ∈ V.
An exact proof term for the current goal is (SepE1 V (λv : set ⇒ Rlt v u0) a HaA).
We prove the intermediate claim HaI: a ∈ unit_interval.
An exact proof term for the current goal is (HVsub a HaV).
We prove the intermediate claim Haconj: ¬ (Rlt a 0) ∧ ¬ (Rlt 1 a).
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) a (HVsub a HaV)).
We prove the intermediate claim Hnlt_1a: ¬ (Rlt 1 a).
An exact proof term for the current goal is (andER (¬ (Rlt a 0)) (¬ (Rlt 1 a)) Haconj).
An exact proof term for the current goal is (RleI a 1 HaR H1R Hnlt_1a).
We prove the intermediate claim Hnlt_l_0: ¬ (Rlt l 0).
An exact proof term for the current goal is (RleE_nlt 0 l H0le_l).
We prove the intermediate claim Hnlt_1_l: ¬ (Rlt 1 l).
An exact proof term for the current goal is (RleE_nlt l 1 Hlub1).
We prove the intermediate claim HlI: l ∈ unit_interval.
An exact proof term for the current goal is (SepI R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) l HlR (andI (¬ (Rlt l 0)) (¬ (Rlt 1 l)) Hnlt_l_0 Hnlt_1_l)).
We prove the intermediate claim HlUV: l ∈ U ∪ V.
rewrite the current goal using Hunion (from left to right).
An exact proof term for the current goal is HlI.
Apply (binunionE U V l HlUV) to the current goal.
Assume HlU: l ∈ U.
We prove the intermediate claim HUopen_in: open_in unit_interval unit_interval_topology U.
An exact proof term for the current goal is (open_inI unit_interval unit_interval_topology U unit_interval_topology_on HUopen).
We prove the intermediate claim HexUamb: ∃Uamb ∈ R_standard_topology, U = Uamb ∩ unit_interval.
An exact proof term for the current goal is (iffEL (open_in unit_interval unit_interval_topology U) (∃Uamb ∈ R_standard_topology, U = Uamb ∩ unit_interval) (open_in_subspace_iff R R_standard_topology unit_interval U R_standard_topology_is_topology unit_interval_sub_R HUsub) HUopen_in).
Apply HexUamb to the current goal.
Let Uamb be given.
Assume HUambpair: Uamb ∈ R_standard_topology ∧ U = Uamb ∩ unit_interval.
We prove the intermediate claim HUambOpen: Uamb ∈ R_standard_topology.
An exact proof term for the current goal is (andEL (Uamb ∈ R_standard_topology) (U = Uamb ∩ unit_interval) HUambpair).
We prove the intermediate claim HUeq: U = Uamb ∩ unit_interval.
An exact proof term for the current goal is (andER (Uamb ∈ R_standard_topology) (U = Uamb ∩ unit_interval) HUambpair).
We prove the intermediate claim HlUamb: l ∈ Uamb.
We prove the intermediate claim HlU2: l ∈ Uamb ∩ unit_interval.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HlU.
An exact proof term for the current goal is (binintersectE1 Uamb unit_interval l HlU2).
We prove the intermediate claim Hexcd: ∃c d : set, c ∈ R ∧ d ∈ R ∧ l ∈ open_interval c d ∧ open_interval c d ⊆ Uamb ∧ Rlt c l ∧ Rlt l d.
An exact proof term for the current goal is (R_standard_open_refine_interval Uamb l HUambOpen HlUamb).
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 ⊆ Uamb) ∧ 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 ⊆ Uamb) ∧ 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 ⊆ Uamb) ∧ 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 ⊆ Uamb).
An exact proof term for the current goal is (andEL (((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) ∧ open_interval c d ⊆ Uamb) (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 ⊆ Uamb) (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 ⊆ Uamb) Hcd2).
We prove the intermediate claim HIntSubUamb: open_interval c d ⊆ Uamb.
An exact proof term for the current goal is (andER ((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) (open_interval c d ⊆ Uamb) Hcd2).
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (andEL (c ∈ R) (d ∈ R) (andEL (c ∈ R ∧ d ∈ R) (l ∈ open_interval c d) Hcd3)).
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (andER (c ∈ R) (d ∈ R) (andEL (c ∈ R ∧ d ∈ R) (l ∈ open_interval c d) Hcd3)).
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 HlS2: SNo l.
An exact proof term for the current goal is HlS.
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
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 Hexeps: ∃Neps ∈ ω, eps_ Neps < gap.
An exact proof term for the current goal is (exists_eps_lt_pos_Euclid gap HgapR HgapPos).
Apply Hexeps to the current goal.
Let Neps be given.
Assume HNepspair.
We prove the intermediate claim HNepsO: Neps ∈ ω.
An exact proof term for the current goal is (andEL (Neps ∈ ω) (eps_ Neps < gap) HNepspair).
We prove the intermediate claim HepsltS: eps_ Neps < gap.
An exact proof term for the current goal is (andER (Neps ∈ ω) (eps_ Neps < gap) HNepspair).
We prove the intermediate claim HepsR: eps_ Neps ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ Neps) (SNo_eps_SNoS_omega Neps HNepsO)).
We prove the intermediate claim HepsposS: 0 < eps_ Neps.
An exact proof term for the current goal is (SNo_eps_pos Neps HNepsO).
We prove the intermediate claim Hepspos: Rlt 0 (eps_ Neps).
An exact proof term for the current goal is (RltI 0 (eps_ Neps) real_0 HepsR HepsposS).
We prove the intermediate claim HepsS: SNo (eps_ Neps).
An exact proof term for the current goal is (real_SNo (eps_ Neps) HepsR).
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 HepsltR: Rlt (eps_ Neps) gap.
An exact proof term for the current goal is (RltI (eps_ Neps) gap HepsR HgapR HepsltS).
We prove the intermediate claim HepsltgapS: eps_ Neps < gap.
An exact proof term for the current goal is (RltE_lt (eps_ Neps) gap HepsltR).
We prove the intermediate claim Hsumlt1: add_SNo (eps_ Neps) c < l.
An exact proof term for the current goal is (add_SNo_minus_Lt2 l c (eps_ Neps) HlS2 HcS HepsS HepsltgapS).
We prove the intermediate claim Hsumlt2: add_SNo c (eps_ Neps) < l.
rewrite the current goal using (add_SNo_com c (eps_ Neps) HcS HepsS) (from left to right).
An exact proof term for the current goal is Hsumlt1.
We prove the intermediate claim Hclm: c < add_SNo l (minus_SNo (eps_ Neps)).
An exact proof term for the current goal is (add_SNo_minus_Lt2b l (eps_ Neps) c HlS2 HepsS HcS Hsumlt2).
We prove the intermediate claim HclmR: add_SNo l (minus_SNo (eps_ Neps)) ∈ R.
An exact proof term for the current goal is (real_add_SNo l HlR (minus_SNo (eps_ Neps)) (real_minus_SNo (eps_ Neps) HepsR)).
We prove the intermediate claim HclmRlt: Rlt c (add_SNo l (minus_SNo (eps_ Neps))).
An exact proof term for the current goal is (RltI c (add_SNo l (minus_SNo (eps_ Neps))) HcR HclmR Hclm).
We prove the intermediate claim Hexa: ∃a : set, a ∈ A ∧ a ∈ R ∧ Rlt (add_SNo l (minus_SNo (eps_ Neps))) a.
An exact proof term for the current goal is (R_lub_approx_from_below A l (eps_ Neps) Hlub HepsR Hepspos).
Apply Hexa to the current goal.
Let a be given.
Assume Haa.
We prove the intermediate claim Haa1: a ∈ A ∧ a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ A ∧ a ∈ R) (Rlt (add_SNo l (minus_SNo (eps_ Neps))) a) Haa).
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (andEL (a ∈ A) (a ∈ R) Haa1).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andER (a ∈ A) (a ∈ R) Haa1).
We prove the intermediate claim Hltlm: Rlt (add_SNo l (minus_SNo (eps_ Neps))) a.
An exact proof term for the current goal is (andER (a ∈ A ∧ a ∈ R) (Rlt (add_SNo l (minus_SNo (eps_ Neps))) a) Haa).
We prove the intermediate claim Hcalt: c < a.
An exact proof term for the current goal is (RltE_lt c a (Rlt_tra c (add_SNo l (minus_SNo (eps_ Neps))) a HclmRlt Hltlm)).
We prove the intermediate claim Hca: Rlt c a.
An exact proof term for the current goal is (RltI c a HcR HaR Hcalt).
We prove the intermediate claim HubA2: ∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 l.
An exact proof term for the current goal is (andER (l ∈ R) (∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 l) Hlubcore).
We prove the intermediate claim Hale_l: Rle a l.
An exact proof term for the current goal is (HubA2 a HaA HaR).
We prove the intermediate claim Hnltla: ¬ (Rlt l a).
An exact proof term for the current goal is (RleE_nlt a l Hale_l).
We prove the intermediate claim Had: Rlt a d.
Apply (SNoLt_trichotomy_or_impred a l (real_SNo a HaR) HlS2 (Rlt a d)) to the current goal.
Assume Haltl: a < l.
We prove the intermediate claim HaltlR: Rlt a l.
An exact proof term for the current goal is (RltI a l HaR HlR Haltl).
An exact proof term for the current goal is (Rlt_tra a l d HaltlR Hld).
Assume Haeq: a = l.
rewrite the current goal using Haeq (from left to right).
An exact proof term for the current goal is Hld.
Assume Hlta: l < a.
We prove the intermediate claim HltaR: Rlt l a.
An exact proof term for the current goal is (RltI l a HlR HaR Hlta).
An exact proof term for the current goal is (FalseE (Hnltla HltaR) (Rlt a d)).
We prove the intermediate claim HaInInt: a ∈ open_interval c d.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt c z ∧ Rlt z d) a HaR (andI (Rlt c a) (Rlt a d) Hca Had)).
We prove the intermediate claim HaUamb: a ∈ Uamb.
An exact proof term for the current goal is (HIntSubUamb a HaInInt).
We prove the intermediate claim HaV: a ∈ V.
An exact proof term for the current goal is (SepE1 V (λv : set ⇒ Rlt v u0) a HaA).
We prove the intermediate claim HaI: a ∈ unit_interval.
An exact proof term for the current goal is (HVsub a HaV).
We prove the intermediate claim HaU: a ∈ U.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (binintersectI Uamb unit_interval a HaUamb HaI).
We prove the intermediate claim HaUV: a ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V a HaU HaV).
We prove the intermediate claim HaE: a ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HaUV.
An exact proof term for the current goal is (EmptyE a HaE).
Assume HlV: l ∈ V.
We prove the intermediate claim Hu0notV: u0 ∉ V.
Assume Hu0V: u0 ∈ V.
We prove the intermediate claim Hu0UV: u0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V u0 Hu0U Hu0V).
We prove the intermediate claim Hu0E: u0 ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is Hu0UV.
An exact proof term for the current goal is (EmptyE u0 Hu0E).
We prove the intermediate claim Hlnequ0: ¬ (l = u0).
Assume Heq: l = u0.
We prove the intermediate claim Hu0V: u0 ∈ V.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HlV.
An exact proof term for the current goal is (Hu0notV Hu0V).
We prove the intermediate claim Hlu0: Rlt l u0.
Apply (SNoLt_trichotomy_or_impred l u0 HlS Hu0S (Rlt l u0)) to the current goal.
Assume Hlt: l < u0.
An exact proof term for the current goal is (RltI l u0 HlR Hu0R Hlt).
Assume Heq: l = u0.
An exact proof term for the current goal is (FalseE (Hlnequ0 Heq) (Rlt l u0)).
Assume Hgt: u0 < l.
We prove the intermediate claim Hu0l: Rlt u0 l.
An exact proof term for the current goal is (RltI u0 l Hu0R HlR Hgt).
We prove the intermediate claim Hnlt: ¬ (Rlt u0 l).
An exact proof term for the current goal is (RleE_nlt l u0 Hlubu0).
An exact proof term for the current goal is (FalseE (Hnlt Hu0l) (Rlt l u0)).
We prove the intermediate claim HVopen_in: open_in unit_interval unit_interval_topology V.
An exact proof term for the current goal is (open_inI unit_interval unit_interval_topology V unit_interval_topology_on HVopen).
We prove the intermediate claim HexVamb: ∃Vamb ∈ R_standard_topology, V = Vamb ∩ unit_interval.
An exact proof term for the current goal is (iffEL (open_in unit_interval unit_interval_topology V) (∃Vamb ∈ R_standard_topology, V = Vamb ∩ unit_interval) (open_in_subspace_iff R R_standard_topology unit_interval V R_standard_topology_is_topology unit_interval_sub_R HVsub) HVopen_in).
Apply HexVamb to the current goal.
Let Vamb be given.
Assume HVambpair: Vamb ∈ R_standard_topology ∧ V = Vamb ∩ unit_interval.
We prove the intermediate claim HVambOpen: Vamb ∈ R_standard_topology.
An exact proof term for the current goal is (andEL (Vamb ∈ R_standard_topology) (V = Vamb ∩ unit_interval) HVambpair).
We prove the intermediate claim HVeq: V = Vamb ∩ unit_interval.
An exact proof term for the current goal is (andER (Vamb ∈ R_standard_topology) (V = Vamb ∩ unit_interval) HVambpair).
We prove the intermediate claim HlVamb: l ∈ Vamb.
We prove the intermediate claim HlV2: l ∈ Vamb ∩ unit_interval.
rewrite the current goal using HVeq (from right to left).
An exact proof term for the current goal is HlV.
An exact proof term for the current goal is (binintersectE1 Vamb unit_interval l HlV2).
We prove the intermediate claim Hexcd: ∃c d : set, c ∈ R ∧ d ∈ R ∧ l ∈ open_interval c d ∧ open_interval c d ⊆ Vamb ∧ Rlt c l ∧ Rlt l d.
An exact proof term for the current goal is (R_standard_open_refine_interval Vamb l HVambOpen HlVamb).
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 ⊆ Vamb) ∧ 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 ⊆ Vamb) ∧ 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 ⊆ Vamb) ∧ 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 ⊆ Vamb).
An exact proof term for the current goal is (andEL (((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) ∧ open_interval c d ⊆ Vamb) (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 ⊆ Vamb) (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 ⊆ Vamb) Hcd2).
We prove the intermediate claim HIntSubVamb: open_interval c d ⊆ Vamb.
An exact proof term for the current goal is (andER ((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) (open_interval c d ⊆ Vamb) Hcd2).
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (andEL (c ∈ R) (d ∈ R) (andEL (c ∈ R ∧ d ∈ R) (l ∈ open_interval c d) Hcd3)).
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (andER (c ∈ R) (d ∈ R) (andEL (c ∈ R ∧ d ∈ R) (l ∈ open_interval c d) Hcd3)).
We prove the intermediate claim HdS: SNo d.
An exact proof term for the current goal is (real_SNo d HdR).
Set gap1 to be the term add_SNo d (minus_SNo l).
Set gap2 to be the term add_SNo u0 (minus_SNo l).
We prove the intermediate claim Hgap1R: gap1 ∈ 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 Hgap2R: gap2 ∈ R.
An exact proof term for the current goal is (real_add_SNo u0 Hu0R (minus_SNo l) (real_minus_SNo l HlR)).
We prove the intermediate claim Hgap1pos: Rlt 0 gap1.
An exact proof term for the current goal is (Rlt_0_diff_of_lt l d Hld).
We prove the intermediate claim Hgap2pos: Rlt 0 gap2.
An exact proof term for the current goal is (Rlt_0_diff_of_lt l u0 Hlu0).
Apply (exists_eps_lt_two_pos_Euclid gap1 gap2 Hgap1R Hgap2R Hgap1pos Hgap2pos) to the current goal.
Let r3 be given.
Assume Hr3pack.
We prove the intermediate claim Hr3p1: (r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 gap1.
An exact proof term for the current goal is (andEL ((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 gap1) (Rlt r3 gap2) Hr3pack).
We prove the intermediate claim Hr3ltgap2: Rlt r3 gap2.
An exact proof term for the current goal is (andER ((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 gap1) (Rlt r3 gap2) Hr3pack).
We prove the intermediate claim Hr3p0: r3 ∈ R ∧ Rlt 0 r3.
An exact proof term for the current goal is (andEL (r3 ∈ R ∧ Rlt 0 r3) (Rlt r3 gap1) Hr3p1).
We prove the intermediate claim Hr3ltgap1: Rlt r3 gap1.
An exact proof term for the current goal is (andER (r3 ∈ R ∧ Rlt 0 r3) (Rlt r3 gap1) Hr3p1).
We prove the intermediate claim Hr3R: r3 ∈ R.
An exact proof term for the current goal is (andEL (r3 ∈ R) (Rlt 0 r3) Hr3p0).
We prove the intermediate claim Hr3pos: Rlt 0 r3.
An exact proof term for the current goal is (andER (r3 ∈ R) (Rlt 0 r3) Hr3p0).
We prove the intermediate claim Hr3S: SNo r3.
An exact proof term for the current goal is (real_SNo r3 Hr3R).
We prove the intermediate claim Hr3posS: 0 < r3.
An exact proof term for the current goal is (RltE_lt 0 r3 Hr3pos).
We prove the intermediate claim Hv1R: add_SNo l r3 ∈ R.
An exact proof term for the current goal is (real_add_SNo l HlR r3 Hr3R).
We prove the intermediate claim Hv1S: SNo (add_SNo l r3).
An exact proof term for the current goal is (real_SNo (add_SNo l r3) Hv1R).
We prove the intermediate claim Hl_lt_v1S: l < add_SNo l r3.
We prove the intermediate claim Hl0: add_SNo l 0 = l.
An exact proof term for the current goal is (add_SNo_0R l HlS).
We prove the intermediate claim Hlt: add_SNo l 0 < add_SNo l r3.
An exact proof term for the current goal is (add_SNo_Lt2 l 0 r3 HlS SNo_0 Hr3S Hr3posS).
rewrite the current goal using Hl0 (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Hl_lt_v1: Rlt l (add_SNo l r3).
An exact proof term for the current goal is (RltI l (add_SNo l r3) HlR Hv1R Hl_lt_v1S).
We prove the intermediate claim Hr3ltgap1S: r3 < gap1.
An exact proof term for the current goal is (RltE_lt r3 gap1 Hr3ltgap1).
We prove the intermediate claim Hgap1S: SNo gap1.
An exact proof term for the current goal is (real_SNo gap1 Hgap1R).
We prove the intermediate claim Hv1lt_dS': add_SNo r3 l < d.
An exact proof term for the current goal is (add_SNo_minus_Lt2 d l r3 HdS HlS Hr3S Hr3ltgap1S).
We prove the intermediate claim Hv1lt_dS: add_SNo l r3 < d.
We prove the intermediate claim Hcom2: add_SNo r3 l = add_SNo l r3.
An exact proof term for the current goal is (add_SNo_com r3 l Hr3S HlS).
rewrite the current goal using Hcom2 (from right to left).
An exact proof term for the current goal is Hv1lt_dS'.
We prove the intermediate claim Hv1lt_d: Rlt (add_SNo l r3) d.
An exact proof term for the current goal is (RltI (add_SNo l r3) d Hv1R HdR Hv1lt_dS).
We prove the intermediate claim Hr3ltgap2S: r3 < gap2.
An exact proof term for the current goal is (RltE_lt r3 gap2 Hr3ltgap2).
We prove the intermediate claim Hgap2S: SNo gap2.
An exact proof term for the current goal is (real_SNo gap2 Hgap2R).
We prove the intermediate claim Hv1lt_u0S': add_SNo r3 l < u0.
An exact proof term for the current goal is (add_SNo_minus_Lt2 u0 l r3 Hu0S HlS Hr3S Hr3ltgap2S).
We prove the intermediate claim Hv1lt_u0S: add_SNo l r3 < u0.
We prove the intermediate claim Hcom3: add_SNo r3 l = add_SNo l r3.
An exact proof term for the current goal is (add_SNo_com r3 l Hr3S HlS).
rewrite the current goal using Hcom3 (from right to left).
An exact proof term for the current goal is Hv1lt_u0S'.
We prove the intermediate claim Hv1lt_u0: Rlt (add_SNo l r3) u0.
An exact proof term for the current goal is (RltI (add_SNo l r3) u0 Hv1R Hu0R Hv1lt_u0S).
We prove the intermediate claim Hv1InInt: add_SNo l r3 ∈ open_interval c d.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt c z ∧ Rlt z d) (add_SNo l r3) Hv1R (andI (Rlt c (add_SNo l r3)) (Rlt (add_SNo l r3) d) (Rlt_tra c l (add_SNo l r3) Hcl Hl_lt_v1) Hv1lt_d)).
We prove the intermediate claim Hv1Vamb: add_SNo l r3 ∈ Vamb.
An exact proof term for the current goal is (HIntSubVamb (add_SNo l r3) Hv1InInt).
We prove the intermediate claim Hu0conj: ¬ (Rlt u0 0) ∧ ¬ (Rlt 1 u0).
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) u0 Hu0I).
We prove the intermediate claim Hnlt_1u0: ¬ (Rlt 1 u0).
An exact proof term for the current goal is (andER (¬ (Rlt u0 0)) (¬ (Rlt 1 u0)) Hu0conj).
We prove the intermediate claim Hu0le1: Rle u0 1.
An exact proof term for the current goal is (RleI u0 1 Hu0R real_1 Hnlt_1u0).
We prove the intermediate claim Hv1le_u0: Rle (add_SNo l r3) u0.
An exact proof term for the current goal is (Rlt_implies_Rle (add_SNo l r3) u0 Hv1lt_u0).
We prove the intermediate claim Hv1le1: Rle (add_SNo l r3) 1.
An exact proof term for the current goal is (Rle_tra (add_SNo l r3) u0 1 Hv1le_u0 Hu0le1).
We prove the intermediate claim Hl_le_v1: Rle l (add_SNo l r3).
An exact proof term for the current goal is (Rlt_implies_Rle l (add_SNo l r3) Hl_lt_v1).
We prove the intermediate claim H0le_v1: Rle 0 (add_SNo l r3).
An exact proof term for the current goal is (Rle_tra 0 l (add_SNo l r3) H0le_l Hl_le_v1).
We prove the intermediate claim Hnlt_v1_0: ¬ (Rlt (add_SNo l r3) 0).
An exact proof term for the current goal is (RleE_nlt 0 (add_SNo l r3) H0le_v1).
We prove the intermediate claim Hnlt_1_v1: ¬ (Rlt 1 (add_SNo l r3)).
An exact proof term for the current goal is (RleE_nlt (add_SNo l r3) 1 Hv1le1).
We prove the intermediate claim Hv1I: add_SNo l r3 ∈ unit_interval.
An exact proof term for the current goal is (SepI R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) (add_SNo l r3) Hv1R (andI (¬ (Rlt (add_SNo l r3) 0)) (¬ (Rlt 1 (add_SNo l r3))) Hnlt_v1_0 Hnlt_1_v1)).
We prove the intermediate claim Hv1V: add_SNo l r3 ∈ V.
rewrite the current goal using HVeq (from left to right).
An exact proof term for the current goal is (binintersectI Vamb unit_interval (add_SNo l r3) Hv1Vamb Hv1I).
We prove the intermediate claim Hv1A: add_SNo l r3 ∈ A.
An exact proof term for the current goal is (SepI V (λv : set ⇒ Rlt v u0) (add_SNo l r3) Hv1V Hv1lt_u0).
We prove the intermediate claim Hv1le_l: Rle (add_SNo l r3) l.
An exact proof term for the current goal is (HubA (add_SNo l r3) Hv1A Hv1R).
We prove the intermediate claim Hnlt: ¬ (Rlt l (add_SNo l r3)).
An exact proof term for the current goal is (RleE_nlt (add_SNo l r3) l Hv1le_l).
An exact proof term for the current goal is (Hnlt Hl_lt_v1).
∎