We will prove topology_on R R_standard_topology ∧ ¬ (∃U V : set, U ∈ R_standard_topology ∧ V ∈ R_standard_topology ∧ separation_of R U V).
Apply andI to the current goal.
An exact proof term for the current goal is R_standard_topology_is_topology.
Assume Hsep: ∃U V : set, U ∈ R_standard_topology ∧ V ∈ R_standard_topology ∧ separation_of R U V.
Apply Hsep to the current goal.
Let U be given.
Assume HexV: ∃V : set, U ∈ R_standard_topology ∧ V ∈ R_standard_topology ∧ separation_of R U V.
Apply HexV to the current goal.
Let V be given.
Assume HUV: U ∈ R_standard_topology ∧ V ∈ R_standard_topology ∧ separation_of R U V.
We prove the intermediate claim HUV0: U ∈ R_standard_topology ∧ V ∈ R_standard_topology.
An exact proof term for the current goal is (andEL (U ∈ R_standard_topology ∧ V ∈ R_standard_topology) (separation_of R U V) HUV).
We prove the intermediate claim HUopen: U ∈ R_standard_topology.
An exact proof term for the current goal is (andEL (U ∈ R_standard_topology) (V ∈ R_standard_topology) HUV0).
We prove the intermediate claim HVopen: V ∈ R_standard_topology.
An exact proof term for the current goal is (andER (U ∈ R_standard_topology) (V ∈ R_standard_topology) HUV0).
We prove the intermediate claim HsepUV: separation_of R U V.
An exact proof term for the current goal is (andER (U ∈ R_standard_topology ∧ V ∈ R_standard_topology) (separation_of R U V) HUV).
We prove the intermediate claim Hpart1: ((((U ∈ 𝒫 R ∧ V ∈ 𝒫 R) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty).
An exact proof term for the current goal is (andEL ((((U ∈ 𝒫 R ∧ V ∈ 𝒫 R) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = R) HsepUV).
We prove the intermediate claim Hunion: U ∪ V = R.
An exact proof term for the current goal is (andER ((((U ∈ 𝒫 R ∧ V ∈ 𝒫 R) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = R) HsepUV).
We prove the intermediate claim HAux: (((U ∈ 𝒫 R ∧ V ∈ 𝒫 R) ∧ U ∩ V = Empty) ∧ U ≠ Empty).
An exact proof term for the current goal is (andEL (((U ∈ 𝒫 R ∧ V ∈ 𝒫 R) ∧ 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 ∈ 𝒫 R ∧ V ∈ 𝒫 R) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) Hpart1).
We prove the intermediate claim Hpowdisj: (U ∈ 𝒫 R ∧ V ∈ 𝒫 R) ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andEL ((U ∈ 𝒫 R ∧ V ∈ 𝒫 R) ∧ 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 ∈ 𝒫 R ∧ V ∈ 𝒫 R) ∧ U ∩ V = Empty) (U ≠ Empty) HAux).
We prove the intermediate claim Hpow: U ∈ 𝒫 R ∧ V ∈ 𝒫 R.
An exact proof term for the current goal is (andEL (U ∈ 𝒫 R ∧ V ∈ 𝒫 R) (U ∩ V = Empty) Hpowdisj).
We prove the intermediate claim Hdisj: U ∩ V = Empty.
An exact proof term for the current goal is (andER (U ∈ 𝒫 R ∧ V ∈ 𝒫 R) (U ∩ V = Empty) Hpowdisj).
We prove the intermediate claim HUpow: U ∈ 𝒫 R.
An exact proof term for the current goal is (andEL (U ∈ 𝒫 R) (V ∈ 𝒫 R) Hpow).
We prove the intermediate claim HVpow: V ∈ 𝒫 R.
An exact proof term for the current goal is (andER (U ∈ 𝒫 R) (V ∈ 𝒫 R) Hpow).
We prove the intermediate claim HUsub: U ⊆ R.
An exact proof term for the current goal is (PowerE R U HUpow).
We prove the intermediate claim HVsub: V ⊆ R.
An exact proof term for the current goal is (PowerE R 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 Hu0R: u0 ∈ R.
An exact proof term for the current goal is (HUsub u0 Hu0U).
We prove the intermediate claim Hv0R: v0 ∈ R.
An exact proof term for the current goal is (HVsub v0 Hv0V).
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).
An exact proof term for the current goal is (HUsub a HaU).
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 HlUV: l ∈ U ∪ V.
rewrite the current goal using Hunion (from left to right).
An exact proof term for the current goal is HlR.
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 Hexcd: ∃c d : set, c ∈ R ∧ d ∈ R ∧ l ∈ open_interval c d ∧ open_interval c d ⊆ U ∧ Rlt c l ∧ Rlt l d.
An exact proof term for the current goal is (R_standard_open_refine_interval U l HUopen HlU).
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 ⊆ U) ∧ 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 ⊆ U) ∧ 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 ⊆ U) ∧ 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 ⊆ U).
An exact proof term for the current goal is (andEL (((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) ∧ open_interval c d ⊆ U) (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 ⊆ U) (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 ⊆ U) Hcd2).
We prove the intermediate claim HIntSubU: open_interval c d ⊆ U.
An exact proof term for the current goal is (andER ((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) (open_interval c d ⊆ U) 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 Hrltd: l < d.
An exact proof term for the current goal is (RltE_lt l d Hld).
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 Hu1U: add_SNo l r3 ∈ U.
An exact proof term for the current goal is (HIntSubU (add_SNo l r3) Hu1InInt).
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 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 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 Hlubcore: l ∈ R ∧ ∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 l.
An exact proof term for the current goal is (andEL (l ∈ R ∧ ∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 l) (∀u : set, u ∈ R → (∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 u) → Rle l u) Hlub).
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 HaV: a ∈ V.
An exact proof term for the current goal is (HIntSubV 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 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) at position 1.
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 Hu0Empty: 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 Hu0Empty).
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).
An exact proof term for the current goal is (HVsub a HaV).
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 HlUV: l ∈ U ∪ V.
rewrite the current goal using Hunion (from left to right).
An exact proof term for the current goal is HlR.
Apply (binunionE U V l HlUV) to the current goal.
Assume HlU: l ∈ U.
We prove the intermediate claim Hexcd: ∃c d : set, c ∈ R ∧ d ∈ R ∧ l ∈ open_interval c d ∧ open_interval c d ⊆ U ∧ Rlt c l ∧ Rlt l d.
An exact proof term for the current goal is (R_standard_open_refine_interval U l HUopen HlU).
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 ⊆ U) ∧ 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 ⊆ U) ∧ 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 ⊆ U) ∧ 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 ⊆ U).
An exact proof term for the current goal is (andEL (((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) ∧ open_interval c d ⊆ U) (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 ⊆ U) (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 ⊆ U) Hcd2).
We prove the intermediate claim HIntSubU: open_interval c d ⊆ U.
An exact proof term for the current goal is (andER ((c ∈ R ∧ d ∈ R) ∧ l ∈ open_interval c d) (open_interval c d ⊆ U) 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 (real_SNo l HlR).
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 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 Hlubcore: l ∈ R ∧ ∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 l.
An exact proof term for the current goal is (andEL (l ∈ R ∧ ∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 l) (∀u : set, u ∈ R → (∀a0 : set, a0 ∈ A → a0 ∈ R → Rle a0 u) → Rle l u) Hlub).
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 HaU: a ∈ U.
An exact proof term for the current goal is (HIntSubU 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 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 HlV: l ∈ V.
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 Hub_u0: ∀a : set, a ∈ A → a ∈ R → Rle a u0.
Let a be given.
Assume HaA: a ∈ A.
Assume HaR: a ∈ R.
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 Hle_l_u0: Rle l u0.
An exact proof term for the current goal is (Hmin u0 Hu0R Hub_u0).
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 Hu0Empty: 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 Hu0Empty).
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 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.
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 (FalseE (Hu0notV Hu0V) (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 Hle_l_u0).
An exact proof term for the current goal is (FalseE (Hnlt Hu0l) (Rlt l u0)).
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 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 Hrltd: l < d.
An exact proof term for the current goal is (RltE_lt l d Hld).
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 Hv1V: add_SNo l r3 ∈ V.
An exact proof term for the current goal is (HIntSubV (add_SNo l r3) Hv1InInt).
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).
∎