We will prove basis_on R R_standard_basis.
We will prove R_standard_basis ⊆ 𝒫 R ∧ (∀x ∈ R, ∃b ∈ R_standard_basis, x ∈ b) ∧ (∀b1 ∈ R_standard_basis, ∀b2 ∈ R_standard_basis, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ R_standard_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2).
Apply and3I to the current goal.
Let U be given.
Assume HU: U ∈ R_standard_basis.
We will prove U ∈ 𝒫 R.
We prove the intermediate claim Hexa: ∃a ∈ R, U ∈ {open_interval a b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) U HU).
Apply Hexa to the current goal.
Let a be given.
Assume Hapair.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R) (U ∈ {open_interval a b|b ∈ R}) Hapair).
We prove the intermediate claim HUfam: U ∈ {open_interval a b|b ∈ R}.
An exact proof term for the current goal is (andER (a ∈ R) (U ∈ {open_interval a b|b ∈ R}) Hapair).
We prove the intermediate claim Hexb: ∃b ∈ R, U = open_interval a b.
An exact proof term for the current goal is (ReplE R (λb0 : set ⇒ open_interval a b0) U HUfam).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (andEL (b ∈ R) (U = open_interval a b) Hbpair).
We prove the intermediate claim HUeq: U = open_interval a b.
An exact proof term for the current goal is (andER (b ∈ R) (U = open_interval a b) Hbpair).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (PowerI R (open_interval a b) (open_interval_Subq_R a b)).
Let x be given.
Assume HxR.
We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
Set a0 to be the term add_SNo x (minus_SNo 1).
Set b0 to be the term add_SNo x 1.
We prove the intermediate claim Ha0R: a0 ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR (minus_SNo 1) Hm1R).
We prove the intermediate claim Hb0R: b0 ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR 1 real_1).
Set I to be the term open_interval a0 b0.
We use I to witness the existential quantifier.
Apply andI to the current goal.
We will prove I ∈ R_standard_basis.
We prove the intermediate claim HIa: I ∈ {open_interval a0 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ open_interval a0 bb) b0 Hb0R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {open_interval aa bb|bb ∈ R}) a0 I Ha0R HIa).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim Hxltb0: x < b0.
We prove the intermediate claim Hx0lt: 0 < 1.
An exact proof term for the current goal is SNoLt_0_1.
We prove the intermediate claim Hx0eq: add_SNo x 0 = x.
An exact proof term for the current goal is (add_SNo_0R x HxS).
We prove the intermediate claim Hlt: add_SNo x 0 < add_SNo x 1.
An exact proof term for the current goal is (add_SNo_Lt2 x 0 1 HxS SNo_0 SNo_1 Hx0lt).
rewrite the current goal using Hx0eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Ha0ltx: a0 < x.
We prove the intermediate claim Hlt: add_SNo x (minus_SNo 1) < add_SNo x 0.
An exact proof term for the current goal is (add_SNo_Lt2 x (minus_SNo 1) 0 HxS Hm1S SNo_0 minus_1_lt_0).
rewrite the current goal using (add_SNo_0R x HxS) (from right to left) at position 2.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Ha0x: Rlt a0 x.
An exact proof term for the current goal is (RltI a0 x Ha0R HxR Ha0ltx).
We prove the intermediate claim Hxb0: Rlt x b0.
An exact proof term for the current goal is (RltI x b0 HxR Hb0R Hxltb0).
We prove the intermediate claim Hconj: Rlt a0 x ∧ Rlt x b0.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0x.
An exact proof term for the current goal is Hxb0.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a0 x0 ∧ Rlt x0 b0) x HxR Hconj).
Let b1 be given.
Assume Hb1.
Let b2 be given.
Assume Hb2.
Let x be given.
Assume Hx1 Hx2.
We prove the intermediate claim Hexa1: ∃a1 ∈ R, b1 ∈ {open_interval a1 b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) b1 Hb1).
We prove the intermediate claim Hexa2: ∃a2 ∈ R, b2 ∈ {open_interval a2 b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) b2 Hb2).
Apply Hexa1 to the current goal.
Let a1 be given.
Assume Ha1pair.
We prove the intermediate claim Ha1R: a1 ∈ R.
An exact proof term for the current goal is (andEL (a1 ∈ R) (b1 ∈ {open_interval a1 b|b ∈ R}) Ha1pair).
We prove the intermediate claim Hb1fam: b1 ∈ {open_interval a1 b|b ∈ R}.
An exact proof term for the current goal is (andER (a1 ∈ R) (b1 ∈ {open_interval a1 b|b ∈ R}) Ha1pair).
We prove the intermediate claim Hexb1: ∃bb1 ∈ R, b1 = open_interval a1 bb1.
An exact proof term for the current goal is (ReplE R (λbb : set ⇒ open_interval a1 bb) b1 Hb1fam).
Apply Hexb1 to the current goal.
Let bb1 be given.
Assume Hbb1pair.
We prove the intermediate claim Hbb1R: bb1 ∈ R.
An exact proof term for the current goal is (andEL (bb1 ∈ R) (b1 = open_interval a1 bb1) Hbb1pair).
We prove the intermediate claim Hb1eq: b1 = open_interval a1 bb1.
An exact proof term for the current goal is (andER (bb1 ∈ R) (b1 = open_interval a1 bb1) Hbb1pair).
Apply Hexa2 to the current goal.
Let a2 be given.
Assume Ha2pair.
We prove the intermediate claim Ha2R: a2 ∈ R.
An exact proof term for the current goal is (andEL (a2 ∈ R) (b2 ∈ {open_interval a2 b|b ∈ R}) Ha2pair).
We prove the intermediate claim Hb2fam: b2 ∈ {open_interval a2 b|b ∈ R}.
An exact proof term for the current goal is (andER (a2 ∈ R) (b2 ∈ {open_interval a2 b|b ∈ R}) Ha2pair).
We prove the intermediate claim Hexb2: ∃bb2 ∈ R, b2 = open_interval a2 bb2.
An exact proof term for the current goal is (ReplE R (λbb : set ⇒ open_interval a2 bb) b2 Hb2fam).
Apply Hexb2 to the current goal.
Let bb2 be given.
Assume Hbb2pair.
We prove the intermediate claim Hbb2R: bb2 ∈ R.
An exact proof term for the current goal is (andEL (bb2 ∈ R) (b2 = open_interval a2 bb2) Hbb2pair).
We prove the intermediate claim Hb2eq: b2 = open_interval a2 bb2.
An exact proof term for the current goal is (andER (bb2 ∈ R) (b2 = open_interval a2 bb2) Hbb2pair).
We prove the intermediate claim HxIn1: x ∈ open_interval a1 bb1.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim HxIn2: x ∈ open_interval a2 bb2.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hx2.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt a1 x0 ∧ Rlt x0 bb1) x HxIn1).
We prove the intermediate claim HxProp1: Rlt a1 x ∧ Rlt x bb1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a1 x0 ∧ Rlt x0 bb1) x HxIn1).
We prove the intermediate claim HxProp2: Rlt a2 x ∧ Rlt x bb2.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a2 x0 ∧ Rlt x0 bb2) x HxIn2).
We prove the intermediate claim Ha1x: Rlt a1 x.
An exact proof term for the current goal is (andEL (Rlt a1 x) (Rlt x bb1) HxProp1).
We prove the intermediate claim Hxbb1: Rlt x bb1.
An exact proof term for the current goal is (andER (Rlt a1 x) (Rlt x bb1) HxProp1).
We prove the intermediate claim Ha2x: Rlt a2 x.
An exact proof term for the current goal is (andEL (Rlt a2 x) (Rlt x bb2) HxProp2).
We prove the intermediate claim Hxbb2: Rlt x bb2.
An exact proof term for the current goal is (andER (Rlt a2 x) (Rlt x bb2) HxProp2).
We prove the intermediate claim Ha1S: SNo a1.
An exact proof term for the current goal is (real_SNo a1 Ha1R).
We prove the intermediate claim Ha2S: SNo a2.
An exact proof term for the current goal is (real_SNo a2 Ha2R).
We prove the intermediate claim Hb1S: SNo bb1.
An exact proof term for the current goal is (real_SNo bb1 Hbb1R).
We prove the intermediate claim Hb2S: SNo bb2.
An exact proof term for the current goal is (real_SNo bb2 Hbb2R).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim Ha1xlt: a1 < x.
An exact proof term for the current goal is (RltE_lt a1 x Ha1x).
We prove the intermediate claim Ha2xlt: a2 < x.
An exact proof term for the current goal is (RltE_lt a2 x Ha2x).
We prove the intermediate claim Hxltbb1: x < bb1.
An exact proof term for the current goal is (RltE_lt x bb1 Hxbb1).
We prove the intermediate claim Hxltbb2: x < bb2.
An exact proof term for the current goal is (RltE_lt x bb2 Hxbb2).
Apply (SNoLt_trichotomy_or_impred a1 a2 Ha1S Ha2S (∃b3 ∈ R_standard_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Ha1lt: a1 < a2.
Apply (SNoLt_trichotomy_or_impred bb1 bb2 Hb1S Hb2S (∃b3 ∈ R_standard_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hb1lt: bb1 < bb2.
Set I3 to be the term open_interval a2 bb1.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {open_interval a2 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ open_interval a2 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {open_interval aa bb|bb ∈ R}) a2 I3 Ha2R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hax: Rlt a2 x.
An exact proof term for the current goal is Ha2x.
We prove the intermediate claim Hxb: Rlt x bb1.
An exact proof term for the current goal is Hxbb1.
We prove the intermediate claim Hconj: Rlt a2 x ∧ Rlt x bb1.
Apply andI to the current goal.
An exact proof term for the current goal is Hax.
An exact proof term for the current goal is Hxb.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a2 z ∧ Rlt z bb1) x HxR Hconj).
Let y be given.
Assume HyI3: y ∈ I3.
We will prove y ∈ b1 ∩ b2.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt a2 z ∧ Rlt z bb1) y HyI3).
We prove the intermediate claim HyProp: Rlt a2 y ∧ Rlt y bb1.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt a2 z ∧ Rlt z bb1) y HyI3).
We prove the intermediate claim Ha2y: Rlt a2 y.
An exact proof term for the current goal is (andEL (Rlt a2 y) (Rlt y bb1) HyProp).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (andER (Rlt a2 y) (Rlt y bb1) HyProp).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim Ha1S': SNo a1.
An exact proof term for the current goal is Ha1S.
We prove the intermediate claim Ha2S': SNo a2.
An exact proof term for the current goal is Ha2S.
We prove the intermediate claim Hbb1S': SNo bb1.
An exact proof term for the current goal is Hb1S.
We prove the intermediate claim Hbb2S': SNo bb2.
An exact proof term for the current goal is Hb2S.
We prove the intermediate claim Ha2ylt: a2 < y.
An exact proof term for the current goal is (RltE_lt a2 y Ha2y).
We prove the intermediate claim Hybb1lt: y < bb1.
An exact proof term for the current goal is (RltE_lt y bb1 Hybb1).
We prove the intermediate claim Hybb2lt: y < bb2.
An exact proof term for the current goal is (SNoLt_tra y bb1 bb2 HyS Hbb1S' Hbb2S' Hybb1lt Hb1lt).
We prove the intermediate claim Hybb2: Rlt y bb2.
An exact proof term for the current goal is (RltI y bb2 HyR Hbb2R Hybb2lt).
We prove the intermediate claim HyIn2: y ∈ open_interval a2 bb2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a2 z ∧ Rlt z bb2) y HyR (andI (Rlt a2 y) (Rlt y bb2) Ha2y Hybb2)).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is HyIn2.
We prove the intermediate claim Ha1ylt: a1 < y.
An exact proof term for the current goal is (SNoLt_tra a1 a2 y Ha1S' Ha2S' HyS Ha1lt Ha2ylt).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (RltI a1 y Ha1R HyR Ha1ylt).
We prove the intermediate claim HyIn1: y ∈ open_interval a1 bb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) y HyR (andI (Rlt a1 y) (Rlt y bb1) Ha1y Hybb1)).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is HyIn1.
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hbeq: bb1 = bb2.
Set I3 to be the term open_interval a2 bb1.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {open_interval a2 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ open_interval a2 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {open_interval aa bb|bb ∈ R}) a2 I3 Ha2R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a2 x ∧ Rlt x bb1.
Apply andI to the current goal.
An exact proof term for the current goal is Ha2x.
An exact proof term for the current goal is Hxbb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a2 z ∧ Rlt z bb1) x HxR Hconj).
Let y be given.
Assume HyI3: y ∈ I3.
We will prove y ∈ b1 ∩ b2.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt a2 z ∧ Rlt z bb1) y HyI3).
We prove the intermediate claim HyProp: Rlt a2 y ∧ Rlt y bb1.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt a2 z ∧ Rlt z bb1) y HyI3).
We prove the intermediate claim Ha2y: Rlt a2 y.
An exact proof term for the current goal is (andEL (Rlt a2 y) (Rlt y bb1) HyProp).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (andER (Rlt a2 y) (Rlt y bb1) HyProp).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim Ha2ylt: a2 < y.
An exact proof term for the current goal is (RltE_lt a2 y Ha2y).
We prove the intermediate claim Hybb1lt: y < bb1.
An exact proof term for the current goal is (RltE_lt y bb1 Hybb1).
We prove the intermediate claim Hybb2: Rlt y bb2.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hybb1.
We prove the intermediate claim HyIn2: y ∈ open_interval a2 bb2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a2 z ∧ Rlt z bb2) y HyR (andI (Rlt a2 y) (Rlt y bb2) Ha2y Hybb2)).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is HyIn2.
We prove the intermediate claim Ha1ylt: a1 < y.
An exact proof term for the current goal is (SNoLt_tra a1 a2 y Ha1S Ha2S HyS Ha1lt Ha2ylt).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (RltI a1 y Ha1R HyR Ha1ylt).
We prove the intermediate claim HyIn1: y ∈ open_interval a1 bb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) y HyR (andI (Rlt a1 y) (Rlt y bb1) Ha1y Hybb1)).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is HyIn1.
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb2lt: bb2 < bb1.
Set I3 to be the term open_interval a2 bb2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {open_interval a2 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ open_interval a2 bb) bb2 Hbb2R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {open_interval aa bb|bb ∈ R}) a2 I3 Ha2R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a2 x ∧ Rlt x bb2.
Apply andI to the current goal.
An exact proof term for the current goal is Ha2x.
An exact proof term for the current goal is Hxbb2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a2 z ∧ Rlt z bb2) x HxR Hconj).
Let y be given.
Assume HyI3: y ∈ I3.
We will prove y ∈ b1 ∩ b2.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt a2 z ∧ Rlt z bb2) y HyI3).
We prove the intermediate claim HyProp: Rlt a2 y ∧ Rlt y bb2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt a2 z ∧ Rlt z bb2) y HyI3).
We prove the intermediate claim Ha2y: Rlt a2 y.
An exact proof term for the current goal is (andEL (Rlt a2 y) (Rlt y bb2) HyProp).
We prove the intermediate claim Hybb2: Rlt y bb2.
An exact proof term for the current goal is (andER (Rlt a2 y) (Rlt y bb2) HyProp).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim Ha2ylt: a2 < y.
An exact proof term for the current goal is (RltE_lt a2 y Ha2y).
We prove the intermediate claim Hybb2lt: y < bb2.
An exact proof term for the current goal is (RltE_lt y bb2 Hybb2).
We prove the intermediate claim Hybb1lt: y < bb1.
An exact proof term for the current goal is (SNoLt_tra y bb2 bb1 HyS Hb2S Hb1S Hybb2lt Hb2lt).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (RltI y bb1 HyR Hbb1R Hybb1lt).
We prove the intermediate claim Ha1ylt: a1 < y.
An exact proof term for the current goal is (SNoLt_tra a1 a2 y Ha1S Ha2S HyS Ha1lt Ha2ylt).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (RltI a1 y Ha1R HyR Ha1ylt).
We prove the intermediate claim HyIn1: y ∈ open_interval a1 bb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) y HyR (andI (Rlt a1 y) (Rlt y bb1) Ha1y Hybb1)).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is HyIn1.
We prove the intermediate claim HyIn2: y ∈ open_interval a2 bb2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a2 z ∧ Rlt z bb2) y HyR (andI (Rlt a2 y) (Rlt y bb2) Ha2y Hybb2)).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is HyIn2.
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Haeq: a1 = a2.
Apply (SNoLt_trichotomy_or_impred bb1 bb2 Hb1S Hb2S (∃b3 ∈ R_standard_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hb1lt: bb1 < bb2.
Set I3 to be the term open_interval a1 bb1.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {open_interval a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ open_interval a1 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {open_interval aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hax: Rlt a1 x.
An exact proof term for the current goal is Ha1x.
We prove the intermediate claim Hconj: Rlt a1 x ∧ Rlt x bb1.
Apply andI to the current goal.
An exact proof term for the current goal is Hax.
An exact proof term for the current goal is Hxbb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) x HxR Hconj).
Let y be given.
Assume HyI3: y ∈ I3.
We will prove y ∈ b1 ∩ b2.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) y HyI3).
We prove the intermediate claim HyProp: Rlt a1 y ∧ Rlt y bb1.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) y HyI3).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (andEL (Rlt a1 y) (Rlt y bb1) HyProp).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (andER (Rlt a1 y) (Rlt y bb1) HyProp).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim Hybb1lt: y < bb1.
An exact proof term for the current goal is (RltE_lt y bb1 Hybb1).
We prove the intermediate claim Hybb2lt: y < bb2.
An exact proof term for the current goal is (SNoLt_tra y bb1 bb2 HyS Hb1S Hb2S Hybb1lt Hb1lt).
We prove the intermediate claim Hybb2: Rlt y bb2.
An exact proof term for the current goal is (RltI y bb2 HyR Hbb2R Hybb2lt).
We prove the intermediate claim HyIn1: y ∈ open_interval a1 bb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) y HyR (andI (Rlt a1 y) (Rlt y bb1) Ha1y Hybb1)).
We prove the intermediate claim HyIn2: y ∈ open_interval a2 bb2.
rewrite the current goal using Haeq (from right to left).
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb2) y HyR (andI (Rlt a1 y) (Rlt y bb2) Ha1y Hybb2)).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is HyIn1.
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is HyIn2.
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hbeq: bb1 = bb2.
Set I3 to be the term open_interval a1 bb1.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {open_interval a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ open_interval a1 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {open_interval aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a1 x ∧ Rlt x bb1.
Apply andI to the current goal.
An exact proof term for the current goal is Ha1x.
An exact proof term for the current goal is Hxbb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) x HxR Hconj).
Let y be given.
Assume HyI3: y ∈ I3.
We will prove y ∈ b1 ∩ b2.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) y HyI3).
We prove the intermediate claim HyProp: Rlt a1 y ∧ Rlt y bb1.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) y HyI3).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (andEL (Rlt a1 y) (Rlt y bb1) HyProp).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (andER (Rlt a1 y) (Rlt y bb1) HyProp).
We prove the intermediate claim Hybb2: Rlt y bb2.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hybb1.
We prove the intermediate claim HyIn1: y ∈ open_interval a1 bb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) y HyR (andI (Rlt a1 y) (Rlt y bb1) Ha1y Hybb1)).
We prove the intermediate claim HyIn2: y ∈ open_interval a2 bb2.
rewrite the current goal using Haeq (from right to left).
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb2) y HyR (andI (Rlt a1 y) (Rlt y bb2) Ha1y Hybb2)).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is HyIn1.
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is HyIn2.
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb2lt: bb2 < bb1.
Set I3 to be the term open_interval a1 bb2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {open_interval a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ open_interval a1 bb) bb2 Hbb2R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {open_interval aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a1 x ∧ Rlt x bb2.
Apply andI to the current goal.
An exact proof term for the current goal is Ha1x.
An exact proof term for the current goal is Hxbb2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb2) x HxR Hconj).
Let y be given.
Assume HyI3: y ∈ I3.
We will prove y ∈ b1 ∩ b2.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb2) y HyI3).
We prove the intermediate claim HyProp: Rlt a1 y ∧ Rlt y bb2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb2) y HyI3).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (andEL (Rlt a1 y) (Rlt y bb2) HyProp).
We prove the intermediate claim Hybb2: Rlt y bb2.
An exact proof term for the current goal is (andER (Rlt a1 y) (Rlt y bb2) HyProp).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim Hybb2lt: y < bb2.
An exact proof term for the current goal is (RltE_lt y bb2 Hybb2).
We prove the intermediate claim Hybb1lt: y < bb1.
An exact proof term for the current goal is (SNoLt_tra y bb2 bb1 HyS Hb2S Hb1S Hybb2lt Hb2lt).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (RltI y bb1 HyR Hbb1R Hybb1lt).
We prove the intermediate claim HyIn1: y ∈ open_interval a1 bb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) y HyR (andI (Rlt a1 y) (Rlt y bb1) Ha1y Hybb1)).
We prove the intermediate claim HyIn2: y ∈ open_interval a2 bb2.
rewrite the current goal using Haeq (from right to left).
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb2) y HyR (andI (Rlt a1 y) (Rlt y bb2) Ha1y Hybb2)).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is HyIn1.
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is HyIn2.
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Ha2lt: a2 < a1.
Apply (SNoLt_trichotomy_or_impred bb1 bb2 Hb1S Hb2S (∃b3 ∈ R_standard_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hb1lt: bb1 < bb2.
Set I3 to be the term open_interval a1 bb1.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {open_interval a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ open_interval a1 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {open_interval aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a1 x ∧ Rlt x bb1.
Apply andI to the current goal.
An exact proof term for the current goal is Ha1x.
An exact proof term for the current goal is Hxbb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) x HxR Hconj).
Let y be given.
Assume HyI3: y ∈ I3.
We will prove y ∈ b1 ∩ b2.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) y HyI3).
We prove the intermediate claim HyProp: Rlt a1 y ∧ Rlt y bb1.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) y HyI3).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (andEL (Rlt a1 y) (Rlt y bb1) HyProp).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (andER (Rlt a1 y) (Rlt y bb1) HyProp).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim Ha1ylt: a1 < y.
An exact proof term for the current goal is (RltE_lt a1 y Ha1y).
We prove the intermediate claim Hybb1lt: y < bb1.
An exact proof term for the current goal is (RltE_lt y bb1 Hybb1).
We prove the intermediate claim Ha2ylt: a2 < y.
An exact proof term for the current goal is (SNoLt_tra a2 a1 y Ha2S Ha1S HyS Ha2lt Ha1ylt).
We prove the intermediate claim Ha2y: Rlt a2 y.
An exact proof term for the current goal is (RltI a2 y Ha2R HyR Ha2ylt).
We prove the intermediate claim Hybb2lt: y < bb2.
An exact proof term for the current goal is (SNoLt_tra y bb1 bb2 HyS Hb1S Hb2S Hybb1lt Hb1lt).
We prove the intermediate claim Hybb2: Rlt y bb2.
An exact proof term for the current goal is (RltI y bb2 HyR Hbb2R Hybb2lt).
We prove the intermediate claim HyIn1: y ∈ open_interval a1 bb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) y HyR (andI (Rlt a1 y) (Rlt y bb1) Ha1y Hybb1)).
We prove the intermediate claim HyIn2: y ∈ open_interval a2 bb2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a2 z ∧ Rlt z bb2) y HyR (andI (Rlt a2 y) (Rlt y bb2) Ha2y Hybb2)).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is HyIn1.
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is HyIn2.
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hbeq: bb1 = bb2.
Set I3 to be the term open_interval a1 bb2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {open_interval a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ open_interval a1 bb) bb2 Hbb2R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {open_interval aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a1 x ∧ Rlt x bb2.
Apply andI to the current goal.
An exact proof term for the current goal is Ha1x.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hxbb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb2) x HxR Hconj).
Let y be given.
Assume HyI3: y ∈ I3.
We will prove y ∈ b1 ∩ b2.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb2) y HyI3).
We prove the intermediate claim HyProp: Rlt a1 y ∧ Rlt y bb2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb2) y HyI3).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (andEL (Rlt a1 y) (Rlt y bb2) HyProp).
We prove the intermediate claim Hybb2: Rlt y bb2.
An exact proof term for the current goal is (andER (Rlt a1 y) (Rlt y bb2) HyProp).
We prove the intermediate claim Hybb1: Rlt y bb1.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is Hybb2.
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim Ha1ylt: a1 < y.
An exact proof term for the current goal is (RltE_lt a1 y Ha1y).
We prove the intermediate claim Ha2ylt: a2 < y.
An exact proof term for the current goal is (SNoLt_tra a2 a1 y Ha2S Ha1S HyS Ha2lt Ha1ylt).
We prove the intermediate claim Ha2y: Rlt a2 y.
An exact proof term for the current goal is (RltI a2 y Ha2R HyR Ha2ylt).
We prove the intermediate claim HyIn1: y ∈ open_interval a1 bb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) y HyR (andI (Rlt a1 y) (Rlt y bb1) Ha1y Hybb1)).
We prove the intermediate claim HyIn2: y ∈ open_interval a2 bb2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a2 z ∧ Rlt z bb2) y HyR (andI (Rlt a2 y) (Rlt y bb2) Ha2y Hybb2)).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is HyIn1.
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is HyIn2.
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb2lt: bb2 < bb1.
Set I3 to be the term open_interval a1 bb2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {open_interval a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ open_interval a1 bb) bb2 Hbb2R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {open_interval aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a1 x ∧ Rlt x bb2.
Apply andI to the current goal.
An exact proof term for the current goal is Ha1x.
An exact proof term for the current goal is Hxbb2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb2) x HxR Hconj).
Let y be given.
Assume HyI3: y ∈ I3.
We will prove y ∈ b1 ∩ b2.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb2) y HyI3).
We prove the intermediate claim HyProp: Rlt a1 y ∧ Rlt y bb2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb2) y HyI3).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (andEL (Rlt a1 y) (Rlt y bb2) HyProp).
We prove the intermediate claim Hybb2: Rlt y bb2.
An exact proof term for the current goal is (andER (Rlt a1 y) (Rlt y bb2) HyProp).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim Ha1ylt: a1 < y.
An exact proof term for the current goal is (RltE_lt a1 y Ha1y).
We prove the intermediate claim Ha2ylt: a2 < y.
An exact proof term for the current goal is (SNoLt_tra a2 a1 y Ha2S Ha1S HyS Ha2lt Ha1ylt).
We prove the intermediate claim Ha2y: Rlt a2 y.
An exact proof term for the current goal is (RltI a2 y Ha2R HyR Ha2ylt).
We prove the intermediate claim Hybb2lt: y < bb2.
An exact proof term for the current goal is (RltE_lt y bb2 Hybb2).
We prove the intermediate claim Hybb1lt: y < bb1.
An exact proof term for the current goal is (SNoLt_tra y bb2 bb1 HyS Hb2S Hb1S Hybb2lt Hb2lt).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (RltI y bb1 HyR Hbb1R Hybb1lt).
We prove the intermediate claim HyIn1: y ∈ open_interval a1 bb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a1 z ∧ Rlt z bb1) y HyR (andI (Rlt a1 y) (Rlt y bb1) Ha1y Hybb1)).
We prove the intermediate claim HyIn2: y ∈ open_interval a2 bb2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a2 z ∧ Rlt z bb2) y HyR (andI (Rlt a2 y) (Rlt y bb2) Ha2y Hybb2)).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is HyIn1.
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is HyIn2.
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
∎