We will prove basis_on R R_lower_limit_basis.
We will prove R_lower_limit_basis ⊆ 𝒫 R ∧ (∀x ∈ R, ∃b ∈ R_lower_limit_basis, x ∈ b) ∧ (∀b1 ∈ R_lower_limit_basis, ∀b2 ∈ R_lower_limit_basis, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ R_lower_limit_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2).
Apply and3I to the current goal.
Let U be given.
Assume HU: U ∈ R_lower_limit_basis.
We will prove U ∈ 𝒫 R.
We prove the intermediate claim Hexa: ∃a ∈ R, U ∈ {halfopen_interval_left a b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {halfopen_interval_left 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 ∈ {halfopen_interval_left a b|b ∈ R}) Hapair).
We prove the intermediate claim HUfam: U ∈ {halfopen_interval_left a b|b ∈ R}.
An exact proof term for the current goal is (andER (a ∈ R) (U ∈ {halfopen_interval_left a b|b ∈ R}) Hapair).
We prove the intermediate claim Hexb: ∃b ∈ R, U = halfopen_interval_left a b.
An exact proof term for the current goal is (ReplE R (λb0 : set ⇒ halfopen_interval_left a b0) U HUfam).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HUeq: U = halfopen_interval_left a b.
An exact proof term for the current goal is (andER (b ∈ R) (U = halfopen_interval_left a b) Hbpair).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (PowerI R (halfopen_interval_left a b) (halfopen_interval_left_Subq_R a b)).
Let x be given.
Assume HxR.
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
Set b0 to be the term add_SNo x 1.
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).
We prove the intermediate claim Hb0S: SNo b0.
An exact proof term for the current goal is (real_SNo b0 Hb0R).
We prove the intermediate claim Hxltb0: x < b0.
We prove the intermediate claim Hx0lt: 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 SNoLt_0_1).
rewrite the current goal using (add_SNo_0R x HxS) (from right to left) at position 1.
An exact proof term for the current goal is Hx0lt.
We prove the intermediate claim Hxb0: Rlt x b0.
An exact proof term for the current goal is (RltI x b0 HxR Hb0R Hxltb0).
Set I to be the term halfopen_interval_left x b0.
We use I to witness the existential quantifier.
Apply andI to the current goal.
We will prove I ∈ R_lower_limit_basis.
We prove the intermediate claim HIa: I ∈ {halfopen_interval_left x bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_left x bb) b0 Hb0R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ R}) x I HxR HIa).
An exact proof term for the current goal is (halfopen_interval_left_leftmem x b0 Hxb0).
Let b1 be given.
Assume Hb1.
Let b2 be given.
Assume Hb2.
Let x be given.
Assume Hx1 Hx2.
We will prove ∃b3 ∈ R_lower_limit_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2.
We prove the intermediate claim Hexa1: ∃a1 ∈ R, b1 ∈ {halfopen_interval_left a1 b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {halfopen_interval_left a0 b|b ∈ R}) b1 Hb1).
Apply Hexa1 to the current goal.
Let a1 be given.
Assume Ha1pair.
Apply Ha1pair to the current goal.
Assume Ha1R: a1 ∈ R.
Assume Hb1fam: b1 ∈ {halfopen_interval_left a1 b|b ∈ R}.
We prove the intermediate claim Hexb1: ∃bb1 ∈ R, b1 = halfopen_interval_left a1 bb1.
An exact proof term for the current goal is (ReplE R (λbb : set ⇒ halfopen_interval_left a1 bb) b1 Hb1fam).
Apply Hexb1 to the current goal.
Let bb1 be given.
Assume Hbb1pair.
Apply Hbb1pair to the current goal.
Assume Hbb1R: bb1 ∈ R.
Assume Hb1eq: b1 = halfopen_interval_left a1 bb1.
We prove the intermediate claim Hexa2: ∃a2 ∈ R, b2 ∈ {halfopen_interval_left a2 b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {halfopen_interval_left a0 b|b ∈ R}) b2 Hb2).
Apply Hexa2 to the current goal.
Let a2 be given.
Assume Ha2pair.
Apply Ha2pair to the current goal.
Assume Ha2R: a2 ∈ R.
Assume Hb2fam: b2 ∈ {halfopen_interval_left a2 b|b ∈ R}.
We prove the intermediate claim Hexb2: ∃bb2 ∈ R, b2 = halfopen_interval_left a2 bb2.
An exact proof term for the current goal is (ReplE R (λbb : set ⇒ halfopen_interval_left a2 bb) b2 Hb2fam).
Apply Hexb2 to the current goal.
Let bb2 be given.
Assume Hbb2pair.
Apply Hbb2pair to the current goal.
Assume Hbb2R: bb2 ∈ R.
Assume Hb2eq: b2 = halfopen_interval_left a2 bb2.
We prove the intermediate claim HxIn1: x ∈ halfopen_interval_left 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 ∈ halfopen_interval_left 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 x0 a1) ∧ Rlt x0 bb1) x HxIn1).
We prove the intermediate claim HxProp1: ¬ (Rlt x a1) ∧ Rlt x bb1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 a1) ∧ Rlt x0 bb1) x HxIn1).
We prove the intermediate claim HxProp2: ¬ (Rlt x a2) ∧ Rlt x bb2.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 a2) ∧ Rlt x0 bb2) x HxIn2).
We prove the intermediate claim Hnxa1: ¬ (Rlt x a1).
An exact proof term for the current goal is (andEL (¬ (Rlt x a1)) (Rlt x bb1) HxProp1).
We prove the intermediate claim Hxbb1: Rlt x bb1.
An exact proof term for the current goal is (andER (¬ (Rlt x a1)) (Rlt x bb1) HxProp1).
We prove the intermediate claim Hnxa2: ¬ (Rlt x a2).
An exact proof term for the current goal is (andEL (¬ (Rlt x a2)) (Rlt x bb2) HxProp2).
We prove the intermediate claim Hxbb2: Rlt x bb2.
An exact proof term for the current goal is (andER (¬ (Rlt x a2)) (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).
Apply (SNoLt_trichotomy_or_impred a1 a2 Ha1S Ha2S (∃b3 ∈ R_lower_limit_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Ha1lt: a1 < a2.
We prove the intermediate claim Ha1a2: Rlt a1 a2.
An exact proof term for the current goal is (RltI a1 a2 Ha1R Ha2R Ha1lt).
Apply (SNoLt_trichotomy_or_impred bb1 bb2 Hb1S Hb2S (∃b3 ∈ R_lower_limit_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hb1lt: bb1 < bb2.
We prove the intermediate claim Hbb1bb2: Rlt bb1 bb2.
An exact proof term for the current goal is (RltI bb1 bb2 Hbb1R Hbb2R Hb1lt).
Set I3 to be the term halfopen_interval_left a2 bb1.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left a2 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_left a2 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ R}) a2 I3 Ha2R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: ¬ (Rlt x a2) ∧ Rlt x bb1.
Apply andI to the current goal.
An exact proof term for the current goal is Hnxa2.
An exact proof term for the current goal is Hxbb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a2) ∧ Rlt z bb1) x HxR Hconj).
Let y be given.
Assume Hy: 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 z a2) ∧ Rlt z bb1) y Hy).
We prove the intermediate claim HyProp: ¬ (Rlt y a2) ∧ Rlt y bb1.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z a2) ∧ Rlt z bb1) y Hy).
We prove the intermediate claim Hnya2: ¬ (Rlt y a2).
An exact proof term for the current goal is (andEL (¬ (Rlt y a2)) (Rlt y bb1) HyProp).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (andER (¬ (Rlt y a2)) (Rlt y bb1) HyProp).
We prove the intermediate claim Hnya1: ¬ (Rlt y a1).
Assume Hya1: Rlt y a1.
We prove the intermediate claim Hya2: Rlt y a2.
An exact proof term for the current goal is (Rlt_tra y a1 a2 Hya1 Ha1a2).
An exact proof term for the current goal is (Hnya2 Hya2).
We prove the intermediate claim Hybb2: Rlt y bb2.
An exact proof term for the current goal is (Rlt_tra y bb1 bb2 Hybb1 Hbb1bb2).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right) at position 1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb1) y HyR (andI (¬ (Rlt y a1)) (Rlt y bb1) Hnya1 Hybb1)).
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 (SepI R (λz : set ⇒ ¬ (Rlt z a2) ∧ Rlt z bb2) y HyR (andI (¬ (Rlt y a2)) (Rlt y bb2) Hnya2 Hybb2)).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume HbbEq: bb1 = bb2.
Set I3 to be the term halfopen_interval_left a2 bb1.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left a2 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_left a2 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ R}) a2 I3 Ha2R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: ¬ (Rlt x a2) ∧ Rlt x bb1.
Apply andI to the current goal.
An exact proof term for the current goal is Hnxa2.
An exact proof term for the current goal is Hxbb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a2) ∧ Rlt z bb1) x HxR Hconj).
Let y be given.
Assume Hy: 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 z a2) ∧ Rlt z bb1) y Hy).
We prove the intermediate claim HyProp: ¬ (Rlt y a2) ∧ Rlt y bb1.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z a2) ∧ Rlt z bb1) y Hy).
We prove the intermediate claim Hnya2: ¬ (Rlt y a2).
An exact proof term for the current goal is (andEL (¬ (Rlt y a2)) (Rlt y bb1) HyProp).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (andER (¬ (Rlt y a2)) (Rlt y bb1) HyProp).
We prove the intermediate claim Hnya1: ¬ (Rlt y a1).
Assume Hya1: Rlt y a1.
We prove the intermediate claim Hya2: Rlt y a2.
An exact proof term for the current goal is (Rlt_tra y a1 a2 Hya1 Ha1a2).
An exact proof term for the current goal is (Hnya2 Hya2).
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 (SepI R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb1) y HyR (andI (¬ (Rlt y a1)) (Rlt y bb1) Hnya1 Hybb1)).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
We prove the intermediate claim Hybb2: Rlt y bb2.
rewrite the current goal using HbbEq (from right to left).
An exact proof term for the current goal is Hybb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a2) ∧ Rlt z bb2) y HyR (andI (¬ (Rlt y a2)) (Rlt y bb2) Hnya2 Hybb2)).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb2lt: bb2 < bb1.
We prove the intermediate claim Hbb2bb1: Rlt bb2 bb1.
An exact proof term for the current goal is (RltI bb2 bb1 Hbb2R Hbb1R Hb2lt).
Set I3 to be the term halfopen_interval_left a2 bb2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left a2 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_left a2 bb) bb2 Hbb2R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ R}) a2 I3 Ha2R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: ¬ (Rlt x a2) ∧ Rlt x bb2.
Apply andI to the current goal.
An exact proof term for the current goal is Hnxa2.
An exact proof term for the current goal is Hxbb2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a2) ∧ Rlt z bb2) x HxR Hconj).
Let y be given.
Assume Hy: 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 z a2) ∧ Rlt z bb2) y Hy).
We prove the intermediate claim HyProp: ¬ (Rlt y a2) ∧ Rlt y bb2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z a2) ∧ Rlt z bb2) y Hy).
We prove the intermediate claim Hnya2: ¬ (Rlt y a2).
An exact proof term for the current goal is (andEL (¬ (Rlt y a2)) (Rlt y bb2) HyProp).
We prove the intermediate claim Hybb2: Rlt y bb2.
An exact proof term for the current goal is (andER (¬ (Rlt y a2)) (Rlt y bb2) HyProp).
We prove the intermediate claim Hnya1: ¬ (Rlt y a1).
Assume Hya1: Rlt y a1.
We prove the intermediate claim Hya2: Rlt y a2.
An exact proof term for the current goal is (Rlt_tra y a1 a2 Hya1 Ha1a2).
An exact proof term for the current goal is (Hnya2 Hya2).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (Rlt_tra y bb2 bb1 Hybb2 Hbb2bb1).
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 (SepI R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb1) y HyR (andI (¬ (Rlt y a1)) (Rlt y bb1) Hnya1 Hybb1)).
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 (SepI R (λz : set ⇒ ¬ (Rlt z a2) ∧ Rlt z bb2) y HyR (andI (¬ (Rlt y a2)) (Rlt y bb2) Hnya2 Hybb2)).
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_lower_limit_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hb1lt: bb1 < bb2.
We prove the intermediate claim Hbb1bb2: Rlt bb1 bb2.
An exact proof term for the current goal is (RltI bb1 bb2 Hbb1R Hbb2R Hb1lt).
Set I3 to be the term halfopen_interval_left a1 bb1.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_left a1 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
An exact proof term for the current goal is HxIn1.
Let y be given.
Assume Hy: 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 z a1) ∧ Rlt z bb1) y Hy).
We prove the intermediate claim HyProp: ¬ (Rlt y a1) ∧ Rlt y bb1.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb1) y Hy).
We prove the intermediate claim Hnya1: ¬ (Rlt y a1).
An exact proof term for the current goal is (andEL (¬ (Rlt y a1)) (Rlt y bb1) HyProp).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (andER (¬ (Rlt y a1)) (Rlt y bb1) HyProp).
We prove the intermediate claim Hybb2: Rlt y bb2.
An exact proof term for the current goal is (Rlt_tra y bb1 bb2 Hybb1 Hbb1bb2).
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 (SepI R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb1) y HyR (andI (¬ (Rlt y a1)) (Rlt y bb1) Hnya1 Hybb1)).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
We prove the intermediate claim Hnya2: ¬ (Rlt y a2).
rewrite the current goal using HaEq (from right to left).
An exact proof term for the current goal is Hnya1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a2) ∧ Rlt z bb2) y HyR (andI (¬ (Rlt y a2)) (Rlt y bb2) Hnya2 Hybb2)).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume HbEq: bb1 = bb2.
We use b1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb1.
Apply andI to the current goal.
An exact proof term for the current goal is Hx1.
Let y be given.
Assume Hy: y ∈ b1.
We will prove y ∈ b1 ∩ b2.
We prove the intermediate claim Hyb2: y ∈ b2.
We prove the intermediate claim Hb1b2: b1 = b2.
rewrite the current goal using Hb1eq (from left to right).
rewrite the current goal using Hb2eq (from left to right).
rewrite the current goal using HaEq (from left to right).
rewrite the current goal using HbEq (from left to right).
Use reflexivity.
rewrite the current goal using Hb1b2 (from right to left).
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is (binintersectI b1 b2 y Hy Hyb2).
Assume Hb2lt: bb2 < bb1.
We prove the intermediate claim Hbb2bb1: Rlt bb2 bb1.
An exact proof term for the current goal is (RltI bb2 bb1 Hbb2R Hbb1R Hb2lt).
Set I3 to be the term halfopen_interval_left a1 bb2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_left a1 bb) bb2 Hbb2R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: ¬ (Rlt x a1) ∧ Rlt x bb2.
Apply andI to the current goal.
An exact proof term for the current goal is Hnxa1.
An exact proof term for the current goal is Hxbb2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb2) x HxR Hconj).
Let y be given.
Assume Hy: 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 z a1) ∧ Rlt z bb2) y Hy).
We prove the intermediate claim HyProp: ¬ (Rlt y a1) ∧ Rlt y bb2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb2) y Hy).
We prove the intermediate claim Hnya1: ¬ (Rlt y a1).
An exact proof term for the current goal is (andEL (¬ (Rlt y a1)) (Rlt y bb2) HyProp).
We prove the intermediate claim Hybb2: Rlt y bb2.
An exact proof term for the current goal is (andER (¬ (Rlt y a1)) (Rlt y bb2) HyProp).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (Rlt_tra y bb2 bb1 Hybb2 Hbb2bb1).
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 (SepI R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb1) y HyR (andI (¬ (Rlt y a1)) (Rlt y bb1) Hnya1 Hybb1)).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
We prove the intermediate claim Hnya2: ¬ (Rlt y a2).
rewrite the current goal using HaEq (from right to left).
An exact proof term for the current goal is Hnya1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a2) ∧ Rlt z bb2) y HyR (andI (¬ (Rlt y a2)) (Rlt y bb2) Hnya2 Hybb2)).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Ha2lt: a2 < a1.
We prove the intermediate claim Ha2a1: Rlt a2 a1.
An exact proof term for the current goal is (RltI a2 a1 Ha2R Ha1R Ha2lt).
Apply (SNoLt_trichotomy_or_impred bb1 bb2 Hb1S Hb2S (∃b3 ∈ R_lower_limit_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hb1lt: bb1 < bb2.
We prove the intermediate claim Hbb1bb2: Rlt bb1 bb2.
An exact proof term for the current goal is (RltI bb1 bb2 Hbb1R Hbb2R Hb1lt).
Set I3 to be the term halfopen_interval_left a1 bb1.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_left a1 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: ¬ (Rlt x a1) ∧ Rlt x bb1.
Apply andI to the current goal.
An exact proof term for the current goal is Hnxa1.
An exact proof term for the current goal is Hxbb1.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb1) x HxR Hconj).
Let y be given.
Assume Hy: 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 z a1) ∧ Rlt z bb1) y Hy).
We prove the intermediate claim HyProp: ¬ (Rlt y a1) ∧ Rlt y bb1.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb1) y Hy).
We prove the intermediate claim Hnya1: ¬ (Rlt y a1).
An exact proof term for the current goal is (andEL (¬ (Rlt y a1)) (Rlt y bb1) HyProp).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (andER (¬ (Rlt y a1)) (Rlt y bb1) HyProp).
We prove the intermediate claim Hnya2: ¬ (Rlt y a2).
Assume Hya2: Rlt y a2.
We prove the intermediate claim Hya1: Rlt y a1.
An exact proof term for the current goal is (Rlt_tra y a2 a1 Hya2 Ha2a1).
An exact proof term for the current goal is (Hnya1 Hya1).
We prove the intermediate claim Hybb2: Rlt y bb2.
An exact proof term for the current goal is (Rlt_tra y bb1 bb2 Hybb1 Hbb1bb2).
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 (SepI R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb1) y HyR (andI (¬ (Rlt y a1)) (Rlt y bb1) Hnya1 Hybb1)).
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 (SepI R (λz : set ⇒ ¬ (Rlt z a2) ∧ Rlt z bb2) y HyR (andI (¬ (Rlt y a2)) (Rlt y bb2) Hnya2 Hybb2)).
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 halfopen_interval_left a1 bb1.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_left a1 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
An exact proof term for the current goal is HxIn1.
Let y be given.
Assume Hy: 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 z a1) ∧ Rlt z bb1) y Hy).
We prove the intermediate claim HyProp: ¬ (Rlt y a1) ∧ Rlt y bb1.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb1) y Hy).
We prove the intermediate claim Hnya1: ¬ (Rlt y a1).
An exact proof term for the current goal is (andEL (¬ (Rlt y a1)) (Rlt y bb1) HyProp).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (andER (¬ (Rlt y a1)) (Rlt y bb1) HyProp).
We prove the intermediate claim Hnya2: ¬ (Rlt y a2).
Assume Hya2: Rlt y a2.
We prove the intermediate claim Hya1: Rlt y a1.
An exact proof term for the current goal is (Rlt_tra y a2 a1 Hya2 Ha2a1).
An exact proof term for the current goal is (Hnya1 Hya1).
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 (SepI R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb1) y HyR (andI (¬ (Rlt y a1)) (Rlt y bb1) Hnya1 Hybb1)).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
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.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a2) ∧ Rlt z bb2) y HyR (andI (¬ (Rlt y a2)) (Rlt y bb2) Hnya2 Hybb2)).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb2lt: bb2 < bb1.
We prove the intermediate claim Hbb2bb1: Rlt bb2 bb1.
An exact proof term for the current goal is (RltI bb2 bb1 Hbb2R Hbb1R Hb2lt).
Set I3 to be the term halfopen_interval_left a1 bb2.
We use I3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HI3fam: I3 ∈ {halfopen_interval_left a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_left a1 bb) bb2 Hbb2R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: ¬ (Rlt x a1) ∧ Rlt x bb2.
Apply andI to the current goal.
An exact proof term for the current goal is Hnxa1.
An exact proof term for the current goal is Hxbb2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb2) x HxR Hconj).
Let y be given.
Assume Hy: 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 z a1) ∧ Rlt z bb2) y Hy).
We prove the intermediate claim HyProp: ¬ (Rlt y a1) ∧ Rlt y bb2.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb2) y Hy).
We prove the intermediate claim Hnya1: ¬ (Rlt y a1).
An exact proof term for the current goal is (andEL (¬ (Rlt y a1)) (Rlt y bb2) HyProp).
We prove the intermediate claim Hybb2: Rlt y bb2.
An exact proof term for the current goal is (andER (¬ (Rlt y a1)) (Rlt y bb2) HyProp).
We prove the intermediate claim Hnya2: ¬ (Rlt y a2).
Assume Hya2: Rlt y a2.
We prove the intermediate claim Hya1: Rlt y a1.
An exact proof term for the current goal is (Rlt_tra y a2 a1 Hya2 Ha2a1).
An exact proof term for the current goal is (Hnya1 Hya1).
We prove the intermediate claim Hybb1: Rlt y bb1.
An exact proof term for the current goal is (Rlt_tra y bb2 bb1 Hybb2 Hbb2bb1).
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 (SepI R (λz : set ⇒ ¬ (Rlt z a1) ∧ Rlt z bb1) y HyR (andI (¬ (Rlt y a1)) (Rlt y bb1) Hnya1 Hybb1)).
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 (SepI R (λz : set ⇒ ¬ (Rlt z a2) ∧ Rlt z bb2) y HyR (andI (¬ (Rlt y a2)) (Rlt y bb2) Hnya2 Hybb2)).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
∎