We will prove basis_on R R_upper_limit_basis.
We will prove R_upper_limit_basis ⊆ 𝒫 R ∧ (∀x ∈ R, ∃b ∈ R_upper_limit_basis, x ∈ b) ∧ (∀b1 ∈ R_upper_limit_basis, ∀b2 ∈ R_upper_limit_basis, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ R_upper_limit_basis, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2).
Apply and3I to the current goal.
Let U be given.
Assume HU: U ∈ R_upper_limit_basis.
We will prove U ∈ 𝒫 R.
We prove the intermediate claim Hexa: ∃a ∈ R, U ∈ {halfopen_interval_right a b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {halfopen_interval_right 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_right a b|b ∈ R}) Hapair).
We prove the intermediate claim HUfam: U ∈ {halfopen_interval_right a b|b ∈ R}.
An exact proof term for the current goal is (andER (a ∈ R) (U ∈ {halfopen_interval_right a b|b ∈ R}) Hapair).
We prove the intermediate claim Hexb: ∃b ∈ R, U = halfopen_interval_right a b.
An exact proof term for the current goal is (ReplE R (λb0 : set ⇒ halfopen_interval_right 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 = halfopen_interval_right a b) Hbpair).
We prove the intermediate claim HUeq: U = halfopen_interval_right a b.
An exact proof term for the current goal is (andER (b ∈ R) (U = halfopen_interval_right 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_right a b) (halfopen_interval_right_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).
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).
Set I to be the term halfopen_interval_right a0 x.
We use I to witness the existential quantifier.
Apply andI to the current goal.
We will prove I ∈ R_upper_limit_basis.
We prove the intermediate claim HIa: I ∈ {halfopen_interval_right a0 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_right a0 bb) x HxR).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_right 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 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 Hnx: ¬ (Rlt x x).
An exact proof term for the current goal is (not_Rlt_refl x HxR).
We prove the intermediate claim Hconj: Rlt a0 x ∧ ¬ (Rlt x x).
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 Hnx.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a0 x0 ∧ ¬ (Rlt x x0)) 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 ∈ {halfopen_interval_right a1 b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {halfopen_interval_right a0 b|b ∈ R}) b1 Hb1).
We prove the intermediate claim Hexa2: ∃a2 ∈ R, b2 ∈ {halfopen_interval_right a2 b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {halfopen_interval_right 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 ∈ {halfopen_interval_right a1 b|b ∈ R}) Ha1pair).
We prove the intermediate claim Hb1fam: b1 ∈ {halfopen_interval_right a1 b|b ∈ R}.
An exact proof term for the current goal is (andER (a1 ∈ R) (b1 ∈ {halfopen_interval_right a1 b|b ∈ R}) Ha1pair).
We prove the intermediate claim Hexb1: ∃bb1 ∈ R, b1 = halfopen_interval_right a1 bb1.
An exact proof term for the current goal is (ReplE R (λbb : set ⇒ halfopen_interval_right 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 = halfopen_interval_right a1 bb1) Hbb1pair).
We prove the intermediate claim Hb1eq: b1 = halfopen_interval_right a1 bb1.
An exact proof term for the current goal is (andER (bb1 ∈ R) (b1 = halfopen_interval_right 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 ∈ {halfopen_interval_right a2 b|b ∈ R}) Ha2pair).
We prove the intermediate claim Hb2fam: b2 ∈ {halfopen_interval_right a2 b|b ∈ R}.
An exact proof term for the current goal is (andER (a2 ∈ R) (b2 ∈ {halfopen_interval_right a2 b|b ∈ R}) Ha2pair).
We prove the intermediate claim Hexb2: ∃bb2 ∈ R, b2 = halfopen_interval_right a2 bb2.
An exact proof term for the current goal is (ReplE R (λbb : set ⇒ halfopen_interval_right 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 = halfopen_interval_right a2 bb2) Hbb2pair).
We prove the intermediate claim Hb2eq: b2 = halfopen_interval_right a2 bb2.
An exact proof term for the current goal is (andER (bb2 ∈ R) (b2 = halfopen_interval_right a2 bb2) Hbb2pair).
We prove the intermediate claim HxIn1: x ∈ halfopen_interval_right 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_right 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 bb1 x0)) x HxIn1).
We prove the intermediate claim HxProp1: Rlt a1 x ∧ ¬ (Rlt bb1 x).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) x HxIn1).
We prove the intermediate claim HxProp2: Rlt a2 x ∧ ¬ (Rlt bb2 x).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb2 x0)) 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 bb1 x)) HxProp1).
We prove the intermediate claim Hnbb1x: ¬ (Rlt bb1 x).
An exact proof term for the current goal is (andER (Rlt a1 x) (¬ (Rlt bb1 x)) HxProp1).
We prove the intermediate claim Ha2x: Rlt a2 x.
An exact proof term for the current goal is (andEL (Rlt a2 x) (¬ (Rlt bb2 x)) HxProp2).
We prove the intermediate claim Hnbb2x: ¬ (Rlt bb2 x).
An exact proof term for the current goal is (andER (Rlt a2 x) (¬ (Rlt bb2 x)) 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_upper_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_upper_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_right 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_right a2 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_right a2 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_right aa bb|bb ∈ R}) a2 I3 Ha2R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a2 x ∧ ¬ (Rlt bb1 x).
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 Hnbb1x.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb1 x0)) 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 (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb1 x0)) y Hy).
We prove the intermediate claim HyProp: Rlt a2 y ∧ ¬ (Rlt bb1 y).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb1 x0)) y Hy).
We prove the intermediate claim Ha2y: Rlt a2 y.
An exact proof term for the current goal is (andEL (Rlt a2 y) (¬ (Rlt bb1 y)) HyProp).
We prove the intermediate claim Hnbb1y: ¬ (Rlt bb1 y).
An exact proof term for the current goal is (andER (Rlt a2 y) (¬ (Rlt bb1 y)) HyProp).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (Rlt_tra a1 a2 y Ha1a2 Ha2y).
We prove the intermediate claim Hnbb2y: ¬ (Rlt bb2 y).
Assume Hbb2y: Rlt bb2 y.
We prove the intermediate claim Hbb1y: Rlt bb1 y.
An exact proof term for the current goal is (Rlt_tra bb1 bb2 y Hbb1bb2 Hbb2y).
An exact proof term for the current goal is (Hnbb1y Hbb1y).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
We prove the intermediate claim Hc1: Rlt a1 y ∧ ¬ (Rlt bb1 y).
Apply andI to the current goal.
An exact proof term for the current goal is Ha1y.
An exact proof term for the current goal is Hnbb1y.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) y HyR Hc1).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
We prove the intermediate claim Hc2: Rlt a2 y ∧ ¬ (Rlt bb2 y).
Apply andI to the current goal.
An exact proof term for the current goal is Ha2y.
An exact proof term for the current goal is Hnbb2y.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb2 x0)) y HyR Hc2).
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_right 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_right a2 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_right a2 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_right aa bb|bb ∈ R}) a2 I3 Ha2R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a2 x ∧ ¬ (Rlt bb1 x).
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 Hnbb1x.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb1 x0)) 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 (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb1 x0)) y Hy).
We prove the intermediate claim HyProp: Rlt a2 y ∧ ¬ (Rlt bb1 y).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb1 x0)) y Hy).
We prove the intermediate claim Ha2y: Rlt a2 y.
An exact proof term for the current goal is (andEL (Rlt a2 y) (¬ (Rlt bb1 y)) HyProp).
We prove the intermediate claim Hnbb1y: ¬ (Rlt bb1 y).
An exact proof term for the current goal is (andER (Rlt a2 y) (¬ (Rlt bb1 y)) HyProp).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (Rlt_tra a1 a2 y Ha1a2 Ha2y).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
We prove the intermediate claim Hc1: Rlt a1 y ∧ ¬ (Rlt bb1 y).
Apply andI to the current goal.
An exact proof term for the current goal is Ha1y.
An exact proof term for the current goal is Hnbb1y.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) y HyR Hc1).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
rewrite the current goal using Hbeq (from right to left).
We prove the intermediate claim Hc2: Rlt a2 y ∧ ¬ (Rlt bb1 y).
Apply andI to the current goal.
An exact proof term for the current goal is Ha2y.
An exact proof term for the current goal is Hnbb1y.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb1 x0)) y HyR Hc2).
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_right 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_right a2 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_right a2 bb) bb2 Hbb2R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_right aa bb|bb ∈ R}) a2 I3 Ha2R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a2 x ∧ ¬ (Rlt bb2 x).
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 Hnbb2x.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb2 x0)) 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 (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb2 x0)) y Hy).
We prove the intermediate claim HyProp: Rlt a2 y ∧ ¬ (Rlt bb2 y).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb2 x0)) y Hy).
We prove the intermediate claim Ha2y: Rlt a2 y.
An exact proof term for the current goal is (andEL (Rlt a2 y) (¬ (Rlt bb2 y)) HyProp).
We prove the intermediate claim Hnbb2y: ¬ (Rlt bb2 y).
An exact proof term for the current goal is (andER (Rlt a2 y) (¬ (Rlt bb2 y)) HyProp).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (Rlt_tra a1 a2 y Ha1a2 Ha2y).
We prove the intermediate claim Hnbb1y: ¬ (Rlt bb1 y).
Assume Hbb1y: Rlt bb1 y.
We prove the intermediate claim Hbb2y: Rlt bb2 y.
An exact proof term for the current goal is (Rlt_tra bb2 bb1 y Hbb2bb1 Hbb1y).
An exact proof term for the current goal is (Hnbb2y Hbb2y).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
We prove the intermediate claim Hc1: Rlt a1 y ∧ ¬ (Rlt bb1 y).
Apply andI to the current goal.
An exact proof term for the current goal is Ha1y.
An exact proof term for the current goal is Hnbb1y.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) y HyR Hc1).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
We prove the intermediate claim Hc2: Rlt a2 y ∧ ¬ (Rlt bb2 y).
Apply andI to the current goal.
An exact proof term for the current goal is Ha2y.
An exact proof term for the current goal is Hnbb2y.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb2 x0)) y HyR Hc2).
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_upper_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_right 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_right a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_right a1 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_right aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a1 x ∧ ¬ (Rlt bb1 x).
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 Hnbb1x.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) 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 (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) y Hy).
We prove the intermediate claim HyProp: Rlt a1 y ∧ ¬ (Rlt bb1 y).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) y Hy).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (andEL (Rlt a1 y) (¬ (Rlt bb1 y)) HyProp).
We prove the intermediate claim Hnbb1y: ¬ (Rlt bb1 y).
An exact proof term for the current goal is (andER (Rlt a1 y) (¬ (Rlt bb1 y)) HyProp).
We prove the intermediate claim Hnbb2y: ¬ (Rlt bb2 y).
Assume Hbb2y: Rlt bb2 y.
We prove the intermediate claim Hbb1y: Rlt bb1 y.
An exact proof term for the current goal is (Rlt_tra bb1 bb2 y Hbb1bb2 Hbb2y).
An exact proof term for the current goal is (Hnbb1y Hbb1y).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
We prove the intermediate claim Hc1: Rlt a1 y ∧ ¬ (Rlt bb1 y).
Apply andI to the current goal.
An exact proof term for the current goal is Ha1y.
An exact proof term for the current goal is Hnbb1y.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) y HyR Hc1).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
rewrite the current goal using Haeq (from right to left).
We prove the intermediate claim Hc2: Rlt a1 y ∧ ¬ (Rlt bb2 y).
Apply andI to the current goal.
An exact proof term for the current goal is Ha1y.
An exact proof term for the current goal is Hnbb2y.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb2 x0)) y HyR Hc2).
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_right 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_right a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_right a1 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_right aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a1 x ∧ ¬ (Rlt bb1 x).
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 Hnbb1x.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) x HxR Hconj).
Let y be given.
Assume Hy: y ∈ I3.
We will prove y ∈ b1 ∩ b2.
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 Hy.
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
rewrite the current goal using Haeq (from right to left).
rewrite the current goal using Hbeq (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 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_right 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_right a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_right a1 bb) bb2 Hbb2R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_right aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a1 x ∧ ¬ (Rlt bb2 x).
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 Hnbb2x.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb2 x0)) 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 (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb2 x0)) y Hy).
We prove the intermediate claim HyProp: Rlt a1 y ∧ ¬ (Rlt bb2 y).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb2 x0)) y Hy).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (andEL (Rlt a1 y) (¬ (Rlt bb2 y)) HyProp).
We prove the intermediate claim Hnbb2y: ¬ (Rlt bb2 y).
An exact proof term for the current goal is (andER (Rlt a1 y) (¬ (Rlt bb2 y)) HyProp).
We prove the intermediate claim Hnbb1y: ¬ (Rlt bb1 y).
Assume Hbb1y: Rlt bb1 y.
We prove the intermediate claim Hbb2y: Rlt bb2 y.
An exact proof term for the current goal is (Rlt_tra bb2 bb1 y Hbb2bb1 Hbb1y).
An exact proof term for the current goal is (Hnbb2y Hbb2y).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
We prove the intermediate claim Hc1: Rlt a1 y ∧ ¬ (Rlt bb1 y).
Apply andI to the current goal.
An exact proof term for the current goal is Ha1y.
An exact proof term for the current goal is Hnbb1y.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) y HyR Hc1).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
rewrite the current goal using Haeq (from right to left).
We prove the intermediate claim Hc2: Rlt a1 y ∧ ¬ (Rlt bb2 y).
Apply andI to the current goal.
An exact proof term for the current goal is Ha1y.
An exact proof term for the current goal is Hnbb2y.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb2 x0)) y HyR Hc2).
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_upper_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_right 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_right a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_right a1 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_right aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a1 x ∧ ¬ (Rlt bb1 x).
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 Hnbb1x.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) 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 (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) y Hy).
We prove the intermediate claim HyProp: Rlt a1 y ∧ ¬ (Rlt bb1 y).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) y Hy).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (andEL (Rlt a1 y) (¬ (Rlt bb1 y)) HyProp).
We prove the intermediate claim Hnbb1y: ¬ (Rlt bb1 y).
An exact proof term for the current goal is (andER (Rlt a1 y) (¬ (Rlt bb1 y)) HyProp).
We prove the intermediate claim Ha2y: Rlt a2 y.
An exact proof term for the current goal is (Rlt_tra a2 a1 y Ha2a1 Ha1y).
We prove the intermediate claim Hnbb2y: ¬ (Rlt bb2 y).
Assume Hbb2y: Rlt bb2 y.
We prove the intermediate claim Hbb1y: Rlt bb1 y.
An exact proof term for the current goal is (Rlt_tra bb1 bb2 y Hbb1bb2 Hbb2y).
An exact proof term for the current goal is (Hnbb1y Hbb1y).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
We prove the intermediate claim Hc1: Rlt a1 y ∧ ¬ (Rlt bb1 y).
Apply andI to the current goal.
An exact proof term for the current goal is Ha1y.
An exact proof term for the current goal is Hnbb1y.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) y HyR Hc1).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
We prove the intermediate claim Hc2: Rlt a2 y ∧ ¬ (Rlt bb2 y).
Apply andI to the current goal.
An exact proof term for the current goal is Ha2y.
An exact proof term for the current goal is Hnbb2y.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb2 x0)) y HyR Hc2).
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_right 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_right a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_right a1 bb) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_right aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a1 x ∧ ¬ (Rlt bb1 x).
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 Hnbb1x.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) 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 (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) y Hy).
We prove the intermediate claim HyProp: Rlt a1 y ∧ ¬ (Rlt bb1 y).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) y Hy).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (andEL (Rlt a1 y) (¬ (Rlt bb1 y)) HyProp).
We prove the intermediate claim Hnbb1y: ¬ (Rlt bb1 y).
An exact proof term for the current goal is (andER (Rlt a1 y) (¬ (Rlt bb1 y)) HyProp).
We prove the intermediate claim Ha2y: Rlt a2 y.
An exact proof term for the current goal is (Rlt_tra a2 a1 y Ha2a1 Ha1y).
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 Hy.
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
We prove the intermediate claim Hnbb2y: ¬ (Rlt bb2 y).
Assume Hbb2y: Rlt bb2 y.
We prove the intermediate claim Hbb1y: Rlt bb1 y.
rewrite the current goal using Hbeq (from left to right) at position 1.
An exact proof term for the current goal is Hbb2y.
An exact proof term for the current goal is (Hnbb1y Hbb1y).
We prove the intermediate claim Hc2: Rlt a2 y ∧ ¬ (Rlt bb2 y).
Apply andI to the current goal.
An exact proof term for the current goal is Ha2y.
An exact proof term for the current goal is Hnbb2y.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb2 x0)) y HyR Hc2).
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_right 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_right a1 bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_right a1 bb) bb2 Hbb2R).
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_right aa bb|bb ∈ R}) a1 I3 Ha1R HI3fam).
Apply andI to the current goal.
We prove the intermediate claim Hconj: Rlt a1 x ∧ ¬ (Rlt bb2 x).
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 Hnbb2x.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb2 x0)) 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 (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb2 x0)) y Hy).
We prove the intermediate claim HyProp: Rlt a1 y ∧ ¬ (Rlt bb2 y).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb2 x0)) y Hy).
We prove the intermediate claim Ha1y: Rlt a1 y.
An exact proof term for the current goal is (andEL (Rlt a1 y) (¬ (Rlt bb2 y)) HyProp).
We prove the intermediate claim Hnbb2y: ¬ (Rlt bb2 y).
An exact proof term for the current goal is (andER (Rlt a1 y) (¬ (Rlt bb2 y)) HyProp).
We prove the intermediate claim Ha2y: Rlt a2 y.
An exact proof term for the current goal is (Rlt_tra a2 a1 y Ha2a1 Ha1y).
We prove the intermediate claim Hnbb1y: ¬ (Rlt bb1 y).
Assume Hbb1y: Rlt bb1 y.
We prove the intermediate claim Hbb2y: Rlt bb2 y.
An exact proof term for the current goal is (Rlt_tra bb2 bb1 y Hbb2bb1 Hbb1y).
An exact proof term for the current goal is (Hnbb2y Hbb2y).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
We prove the intermediate claim Hc1: Rlt a1 y ∧ ¬ (Rlt bb1 y).
Apply andI to the current goal.
An exact proof term for the current goal is Ha1y.
An exact proof term for the current goal is Hnbb1y.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a1 x0 ∧ ¬ (Rlt bb1 x0)) y HyR Hc1).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
We prove the intermediate claim Hc2: Rlt a2 y ∧ ¬ (Rlt bb2 y).
Apply andI to the current goal.
An exact proof term for the current goal is Ha2y.
An exact proof term for the current goal is Hnbb2y.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a2 x0 ∧ ¬ (Rlt bb2 x0)) y HyR Hc2).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
∎