We will prove (unit_interval_left_half ∩ unit_interval_right_half) = {eps_ 1}.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ (unit_interval_left_half ∩ unit_interval_right_half).
We will prove t ∈ {eps_ 1}.
We prove the intermediate claim HtL: t ∈ unit_interval_left_half.
An exact proof term for the current goal is (binintersectE1 unit_interval_left_half unit_interval_right_half t Ht).
We prove the intermediate claim HtR: t ∈ unit_interval_right_half.
An exact proof term for the current goal is (binintersectE2 unit_interval_left_half unit_interval_right_half t Ht).
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (unit_interval_left_half_sub t HtL).
We prove the intermediate claim HtReal: t ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R t HtI).
We prove the intermediate claim HeReal: eps_ 1 ∈ R.
An exact proof term for the current goal is eps_1_in_R.
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtReal).
We prove the intermediate claim HeS: SNo (eps_ 1).
An exact proof term for the current goal is (real_SNo (eps_ 1) HeReal).
We prove the intermediate claim Hnlt_et: ¬ (Rlt (eps_ 1) t).
An exact proof term for the current goal is (SepE2 unit_interval (λt0 : set ⇒ ¬ (Rlt (eps_ 1) t0)) t HtL).
We prove the intermediate claim Hnlt_te: ¬ (Rlt t (eps_ 1)).
An exact proof term for the current goal is (SepE2 unit_interval (λt0 : set ⇒ ¬ (Rlt t0 (eps_ 1))) t HtR).
Apply (SNoLt_trichotomy_or_impred t (eps_ 1) HtS HeS (t ∈ {eps_ 1})) to the current goal.
Assume HtltS: t < (eps_ 1).
We prove the intermediate claim Htlt: Rlt t (eps_ 1).
An exact proof term for the current goal is (RltI t (eps_ 1) HtReal HeReal HtltS).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_te Htlt).
Assume Heq: t = eps_ 1.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SingI (eps_ 1)).
Assume HeltS: (eps_ 1) < t.
We prove the intermediate claim Helt: Rlt (eps_ 1) t.
An exact proof term for the current goal is (RltI (eps_ 1) t HeReal HtReal HeltS).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_et Helt).
Let t be given.
Assume Ht: t ∈ {eps_ 1}.
We will prove t ∈ (unit_interval_left_half ∩ unit_interval_right_half).
We prove the intermediate claim Hteq: t = eps_ 1.
An exact proof term for the current goal is (SingE (eps_ 1) t Ht).
rewrite the current goal using Hteq (from left to right).
We prove the intermediate claim HeI: eps_ 1 ∈ unit_interval.
An exact proof term for the current goal is eps_1_in_unit_interval.
We prove the intermediate claim Hnlt_e: ¬ (Rlt (eps_ 1) (eps_ 1)).
An exact proof term for the current goal is (not_Rlt_refl (eps_ 1) eps_1_in_R).
We prove the intermediate claim Hnlt_e2: ¬ (Rlt (eps_ 1) (eps_ 1)).
An exact proof term for the current goal is (not_Rlt_refl (eps_ 1) eps_1_in_R).
We prove the intermediate claim HeL: eps_ 1 ∈ unit_interval_left_half.
An exact proof term for the current goal is (SepI unit_interval (λt0 : set ⇒ ¬ (Rlt (eps_ 1) t0)) (eps_ 1) HeI Hnlt_e).
We prove the intermediate claim HeR: eps_ 1 ∈ unit_interval_right_half.
An exact proof term for the current goal is (SepI unit_interval (λt0 : set ⇒ ¬ (Rlt t0 (eps_ 1))) (eps_ 1) HeI Hnlt_e2).
An exact proof term for the current goal is (binintersectI unit_interval_left_half unit_interval_right_half (eps_ 1) HeL HeR).
∎