We will prove boundary_of (setprod R R) R2_standard_topology ordered_square_open_strip ≠ boundary_of (setprod R R) R2_dictionary_order_topology ordered_square_open_strip.
Assume Heq: boundary_of (setprod R R) R2_standard_topology ordered_square_open_strip = boundary_of (setprod R R) R2_dictionary_order_topology ordered_square_open_strip.
We will prove False.
Set X to be the term setprod R R.
Set A to be the term ordered_square_open_strip.
We prove the intermediate claim Hexq: ∃q ∈ rational_numbers, Rlt (eps_ 1) q ∧ Rlt q 1.
An exact proof term for the current goal is (rational_dense_between_reals (eps_ 1) 1 eps_1_in_R real_1 eps_1_lt1_R).
Apply Hexq to the current goal.
Let q be given.
Assume Hqpack.
Apply Hqpack to the current goal.
Assume HqQ Hqineq.
We prove the intermediate claim HepsLtq: Rlt (eps_ 1) q.
An exact proof term for the current goal is (andEL (Rlt (eps_ 1) q) (Rlt q 1) Hqineq).
We prove the intermediate claim HqLt1: Rlt q 1.
An exact proof term for the current goal is (andER (Rlt (eps_ 1) q) (Rlt q 1) Hqineq).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
Set p to be the term (eps_ 1,q).
We prove the intermediate claim HpX: p ∈ X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (eps_ 1) q eps_1_in_R HqR).
We prove the intermediate claim Hqpos: Rlt 0 q.
An exact proof term for the current goal is (Rlt_tra 0 (eps_ 1) q eps_1_pos_R HepsLtq).
We prove the intermediate claim Hnltq0: ¬ (Rlt q 0).
An exact proof term for the current goal is (not_Rlt_sym 0 q Hqpos).
We prove the intermediate claim Hnlt1q: ¬ (Rlt 1 q).
An exact proof term for the current goal is (not_Rlt_sym q 1 HqLt1).
We prove the intermediate claim HqUI: q ∈ unit_interval.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) q HqR (andI (¬ (Rlt q 0)) (¬ (Rlt 1 q)) Hnltq0 Hnlt1q)).
We prove the intermediate claim HpSq: p ∈ ordered_square.
We prove the intermediate claim Hsqdef: ordered_square = setprod unit_interval unit_interval.
Use reflexivity.
rewrite the current goal using Hsqdef (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval (eps_ 1) q eps_1_in_unit_interval HqUI).
We prove the intermediate claim HpA: p ∈ A.
We prove the intermediate claim HAdef: A = {p0 ∈ ordered_square|∃y : set, p0 = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)}.
Use reflexivity.
rewrite the current goal using HAdef (from left to right).
Apply (SepI ordered_square (λp0 : set ⇒ ∃y : set, p0 = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)) p HpSq) to the current goal.
We use q to witness the existential quantifier.
We will prove p = (eps_ 1,q) ∧ Rlt (eps_ 1) q ∧ ¬ (Rlt 1 q).
Apply andI to the current goal.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is HepsLtq.
An exact proof term for the current goal is Hnlt1q.
We prove the intermediate claim HtopStd: topology_on X R2_standard_topology.
An exact proof term for the current goal is (product_topology_is_topology R R_standard_topology R R_standard_topology R_standard_topology_is_topology R_standard_topology_is_topology).
We prove the intermediate claim HAsubX: A ⊆ X.
Let r be given.
Assume HrA: r ∈ A.
We will prove r ∈ X.
We prove the intermediate claim HrSq: r ∈ ordered_square.
An exact proof term for the current goal is (SepE1 ordered_square (λp0 : set ⇒ ∃y : set, p0 = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)) r HrA).
We prove the intermediate claim HsqSub: ordered_square ⊆ X.
We prove the intermediate claim Hsqdef: ordered_square = setprod unit_interval unit_interval.
Use reflexivity.
rewrite the current goal using Hsqdef (from left to right).
An exact proof term for the current goal is (setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R).
An exact proof term for the current goal is (HsqSub r HrSq).
We prove the intermediate claim HpclA_std: p ∈ closure_of X R2_standard_topology A.
We prove the intermediate claim HAcl: A ⊆ closure_of X R2_standard_topology A.
An exact proof term for the current goal is (subset_of_closure X R2_standard_topology A HtopStd HAsubX).
An exact proof term for the current goal is (HAcl p HpA).
We prove the intermediate claim HpclComp_std: p ∈ closure_of X R2_standard_topology (X ∖ A).
We will prove p ∈ closure_of X R2_standard_topology (X ∖ A).
We prove the intermediate claim Hcldef: closure_of X R2_standard_topology (X ∖ A) = {x ∈ X|∀U : set, U ∈ R2_standard_topology → x ∈ U → U ∩ (X ∖ A) ≠ Empty}.
Use reflexivity.
rewrite the current goal using Hcldef (from left to right).
Apply (SepI X (λx0 : set ⇒ ∀U : set, U ∈ R2_standard_topology → x0 ∈ U → U ∩ (X ∖ A) ≠ Empty) p HpX) to the current goal.
Let U be given.
Assume HU: U ∈ R2_standard_topology.
Assume HpU: p ∈ U.
We will prove U ∩ (X ∖ A) ≠ Empty.
Set B to be the term product_subbasis R R_standard_topology R R_standard_topology.
We prove the intermediate claim HUgen: U ∈ generated_topology (setprod R R) B.
An exact proof term for the current goal is HU.
We prove the intermediate claim HUprop: ∀x ∈ U, ∃b ∈ B, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ B, x0 ∈ b0 ∧ b0 ⊆ U0) U HUgen).
We prove the intermediate claim Hexb: ∃b ∈ B, p ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (HUprop p HpU).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
Apply Hbpair to the current goal.
Assume HbB Hbprop.
We prove the intermediate claim Hpb: p ∈ b.
An exact proof term for the current goal is (andEL (p ∈ b) (b ⊆ U) Hbprop).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (p ∈ b) (b ⊆ U) Hbprop).
Apply (famunionE_impred R_standard_topology (λU0 : set ⇒ {rectangle_set U0 V|V ∈ R_standard_topology}) b HbB (U ∩ (X ∖ A) ≠ Empty)) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ R_standard_topology.
Assume HbIn: b ∈ {rectangle_set U0 V|V ∈ R_standard_topology}.
Apply (ReplE_impred R_standard_topology (λV0 : set ⇒ rectangle_set U0 V0) b HbIn (U ∩ (X ∖ A) ≠ Empty)) to the current goal.
Let V0 be given.
Assume HV0: V0 ∈ R_standard_topology.
Assume Hbeq: b = rectangle_set U0 V0.
We prove the intermediate claim HpbUV: p ∈ rectangle_set U0 V0.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hpb.
We prove the intermediate claim HpUV: p ∈ setprod U0 V0.
rewrite the current goal using rectangle_set_def (from right to left).
An exact proof term for the current goal is HpbUV.
We prove the intermediate claim Hp0U0: p 0 ∈ U0.
An exact proof term for the current goal is (ap0_Sigma U0 (λ_ : set ⇒ V0) p HpUV).
We prove the intermediate claim Hp1V0: p 1 ∈ V0.
An exact proof term for the current goal is (ap1_Sigma U0 (λ_ : set ⇒ V0) p HpUV).
We prove the intermediate claim Hp0eq: p 0 = eps_ 1.
An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) q).
We prove the intermediate claim Hp1eq: p 1 = q.
An exact proof term for the current goal is (tuple_2_1_eq (eps_ 1) q).
We prove the intermediate claim HepsU0: eps_ 1 ∈ U0.
rewrite the current goal using Hp0eq (from right to left).
An exact proof term for the current goal is Hp0U0.
We prove the intermediate claim HqV0: q ∈ V0.
rewrite the current goal using Hp1eq (from right to left).
An exact proof term for the current goal is Hp1V0.
Apply (xm (∃x : set, x ∈ U0 ∧ x ≠ eps_ 1)) to the current goal.
Assume Hexx: ∃x : set, x ∈ U0 ∧ x ≠ eps_ 1.
Apply Hexx to the current goal.
Let x be given.
Assume Hxcore.
Apply Hxcore to the current goal.
Assume HxU0 Hxneq.
Set r to be the term (x,q).
We prove the intermediate claim HrUV: r ∈ setprod U0 V0.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma U0 V0 x q HxU0 HqV0).
We prove the intermediate claim HrB: r ∈ b.
rewrite the current goal using Hbeq (from left to right).
rewrite the current goal using rectangle_set_def (from right to left).
An exact proof term for the current goal is HrUV.
We prove the intermediate claim HrU: r ∈ U.
An exact proof term for the current goal is (HbsubU r HrB).
We prove the intermediate claim HrX: r ∈ X.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is ((topology_elem_subset R R_standard_topology U0 R_standard_topology_is_topology HU0) x HxU0).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x q HxR HqR).
We prove the intermediate claim HrnotA: r ∉ A.
Assume HrA: r ∈ A.
We prove the intermediate claim HrSq: r ∈ ordered_square.
An exact proof term for the current goal is (SepE1 ordered_square (λp0 : set ⇒ ∃y : set, p0 = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)) r HrA).
We prove the intermediate claim Hexy: ∃y : set, r = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y).
An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃y : set, p0 = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)) r HrA).
Apply Hexy to the current goal.
Let y be given.
Assume Hyprop.
We prove the intermediate claim Hpair: r = (eps_ 1,y) ∧ Rlt (eps_ 1) y.
An exact proof term for the current goal is (andEL (r = (eps_ 1,y) ∧ Rlt (eps_ 1) y) (¬ (Rlt 1 y)) Hyprop).
We prove the intermediate claim Hreps: r = (eps_ 1,y).
An exact proof term for the current goal is (andEL (r = (eps_ 1,y)) (Rlt (eps_ 1) y) Hpair).
We prove the intermediate claim H0eq: r 0 = eps_ 1.
rewrite the current goal using Hreps (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) y).
We prove the intermediate claim Hr0: r 0 = x.
An exact proof term for the current goal is (tuple_2_0_eq x q).
We prove the intermediate claim Heq: x = eps_ 1.
rewrite the current goal using Hr0 (from right to left).
An exact proof term for the current goal is H0eq.
An exact proof term for the current goal is (Hxneq Heq).
We prove the intermediate claim HrComp: r ∈ X ∖ A.
An exact proof term for the current goal is (setminusI X A r HrX HrnotA).
We prove the intermediate claim HrInt: r ∈ U ∩ (X ∖ A).
An exact proof term for the current goal is (binintersectI U (X ∖ A) r HrU HrComp).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ (X ∖ A)) r HrInt).
Assume Hno.
We will prove U ∩ (X ∖ A) ≠ Empty.
We prove the intermediate claim HU0sub: U0 ⊆ {eps_ 1}.
Let t be given.
Assume HtU0: t ∈ U0.
We will prove t ∈ {eps_ 1}.
Apply (xm (t = eps_ 1)) to the current goal.
Assume Hteq.
rewrite the current goal using Hteq (from left to right).
An exact proof term for the current goal is (SingI (eps_ 1)).
Assume Htneq.
Apply FalseE to the current goal.
Apply Hno to the current goal.
We use t to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HtU0.
An exact proof term for the current goal is Htneq.
We prove the intermediate claim HsingSub: {eps_ 1} ⊆ U0.
Let t be given.
Assume Ht: t ∈ {eps_ 1}.
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).
An exact proof term for the current goal is HepsU0.
We prove the intermediate claim HU0eq: U0 = {eps_ 1}.
Apply set_ext to the current goal.
An exact proof term for the current goal is HU0sub.
An exact proof term for the current goal is HsingSub.
We prove the intermediate claim HsingOpen: {eps_ 1} ∈ R_standard_topology.
rewrite the current goal using HU0eq (from right to left).
An exact proof term for the current goal is HU0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (singleton_not_open_R_standard_topology (eps_ 1) eps_1_in_R HsingOpen).
We prove the intermediate claim Hpbd_std: p ∈ boundary_of X R2_standard_topology A.
We prove the intermediate claim Hbddef: boundary_of X R2_standard_topology A = closure_of X R2_standard_topology A ∩ closure_of X R2_standard_topology (X ∖ A).
Use reflexivity.
rewrite the current goal using Hbddef (from left to right).
An exact proof term for the current goal is (binintersectI (closure_of X R2_standard_topology A) (closure_of X R2_standard_topology (X ∖ A)) p HpclA_std HpclComp_std).
We prove the intermediate claim Hpnot_bd_dic: ¬ (p ∈ boundary_of X R2_dictionary_order_topology A).
Assume Hpbd: p ∈ boundary_of X R2_dictionary_order_topology A.
We will prove False.
We prove the intermediate claim Hbddef: boundary_of X R2_dictionary_order_topology A = closure_of X R2_dictionary_order_topology A ∩ closure_of X R2_dictionary_order_topology (X ∖ A).
Use reflexivity.
We prove the intermediate claim Hpbd': p ∈ closure_of X R2_dictionary_order_topology A ∩ closure_of X R2_dictionary_order_topology (X ∖ A).
rewrite the current goal using Hbddef (from right to left).
An exact proof term for the current goal is Hpbd.
We prove the intermediate claim HpclComp: p ∈ closure_of X R2_dictionary_order_topology (X ∖ A).
An exact proof term for the current goal is (binintersectE2 (closure_of X R2_dictionary_order_topology A) (closure_of X R2_dictionary_order_topology (X ∖ A)) p Hpbd').
We prove the intermediate claim Hpcond: ∀U : set, U ∈ R2_dictionary_order_topology → p ∈ U → U ∩ (X ∖ A) ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U : set, U ∈ R2_dictionary_order_topology → x0 ∈ U → U ∩ (X ∖ A) ≠ Empty) p HpclComp).
Set a to be the term (eps_ 1,eps_ 1).
Set b to be the term (eps_ 1,1).
Set W to be the term {x ∈ X|order_rel X a x ∧ order_rel X x b}.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (eps_ 1) (eps_ 1) eps_1_in_R eps_1_in_R).
We prove the intermediate claim HbX: b ∈ X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (eps_ 1) 1 eps_1_in_R real_1).
We prove the intermediate claim HtopDic: topology_on X R2_dictionary_order_topology.
An exact proof term for the current goal is dictionary_order_topology_is_topology.
We prove the intermediate claim HWopen: W ∈ R2_dictionary_order_topology.
Set U1 to be the term open_ray_upper X a.
Set U2 to be the term open_ray_lower X b.
We prove the intermediate claim HU1S: U1 ∈ open_rays_subbasis X.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis X a HaX).
We prove the intermediate claim HU2S: U2 ∈ open_rays_subbasis X.
An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis X b HbX).
We prove the intermediate claim HU1open: U1 ∈ R2_dictionary_order_topology.
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis X (open_rays_subbasis X) U1 (open_rays_subbasis_is_subbasis X) HU1S).
We prove the intermediate claim HU2open: U2 ∈ R2_dictionary_order_topology.
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis X (open_rays_subbasis X) U2 (open_rays_subbasis_is_subbasis X) HU2S).
We prove the intermediate claim HWeq: W = U1 ∩ U2.
We prove the intermediate claim HdefW: W = {x ∈ X|order_rel X a x ∧ order_rel X x b}.
Use reflexivity.
rewrite the current goal using HdefW (from left to right).
An exact proof term for the current goal is (open_interval_eq_rays_intersection X a b).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is (topology_binintersect_closed X R2_dictionary_order_topology U1 U2 HtopDic HU1open HU2open).
We prove the intermediate claim HpW: p ∈ W.
Apply (SepI X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) p HpX) to the current goal.
We will prove order_rel X a p ∧ order_rel X p b.
We prove the intermediate claim HepsRefl: (eps_ 1) = (eps_ 1).
Use reflexivity.
Apply andI to the current goal.
We prove the intermediate claim HaEq: a = (eps_ 1,eps_ 1).
Use reflexivity.
We prove the intermediate claim HpEq: p = (eps_ 1,q).
Use reflexivity.
rewrite the current goal using HaEq (from left to right).
rewrite the current goal using HpEq (from left to right).
An exact proof term for the current goal is (order_rel_setprod_R_R_intro (eps_ 1) (eps_ 1) (eps_ 1) q (orIR (Rlt (eps_ 1) (eps_ 1)) ((eps_ 1) = (eps_ 1) ∧ Rlt (eps_ 1) q) (andI ((eps_ 1) = (eps_ 1)) (Rlt (eps_ 1) q) HepsRefl HepsLtq))).
We prove the intermediate claim HpEq: p = (eps_ 1,q).
Use reflexivity.
We prove the intermediate claim HbEq: b = (eps_ 1,1).
Use reflexivity.
rewrite the current goal using HpEq (from left to right).
rewrite the current goal using HbEq (from left to right).
An exact proof term for the current goal is (order_rel_setprod_R_R_intro (eps_ 1) q (eps_ 1) 1 (orIR (Rlt (eps_ 1) (eps_ 1)) ((eps_ 1) = (eps_ 1) ∧ Rlt q 1) (andI ((eps_ 1) = (eps_ 1)) (Rlt q 1) HepsRefl HqLt1))).
We prove the intermediate claim HWsubA: W ⊆ A.
Let x be given.
Assume HxW: x ∈ W.
We will prove x ∈ A.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) x HxW).
We prove the intermediate claim Hrel: order_rel X a x ∧ order_rel X x b.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) x HxW).
We prove the intermediate claim Hrel1: order_rel X a x.
An exact proof term for the current goal is (andEL (order_rel X a x) (order_rel X x b) Hrel).
We prove the intermediate claim Hrel2: order_rel X x b.
An exact proof term for the current goal is (andER (order_rel X a x) (order_rel X x b) Hrel).
We prove the intermediate claim Hex1: ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ x = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).
An exact proof term for the current goal is (order_rel_setprod_R_R_unfold a x Hrel1).
We prove the intermediate claim Hex2: ∃a1 a2 b1 b2 : set, x = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).
An exact proof term for the current goal is (order_rel_setprod_R_R_unfold x b Hrel2).
Apply Hex1 to the current goal.
Let a1 be given.
Assume Ha1pack.
Apply Ha1pack to the current goal.
Let a2 be given.
Assume Ha2pack.
Apply Ha2pack to the current goal.
Let x1 be given.
Assume Hx1pack.
Apply Hx1pack to the current goal.
Let x2 be given.
Assume Hcore1.
We prove the intermediate claim Hax: a = (a1,a2) ∧ x = (x1,x2).
An exact proof term for the current goal is (andEL (a = (a1,a2) ∧ x = (x1,x2)) (Rlt a1 x1 ∨ (a1 = x1 ∧ Rlt a2 x2)) Hcore1).
We prove the intermediate claim Ha_eq: a = (a1,a2).
An exact proof term for the current goal is (andEL (a = (a1,a2)) (x = (x1,x2)) Hax).
We prove the intermediate claim Hx_eq: x = (x1,x2).
An exact proof term for the current goal is (andER (a = (a1,a2)) (x = (x1,x2)) Hax).
We prove the intermediate claim Hlex1: Rlt a1 x1 ∨ (a1 = x1 ∧ Rlt a2 x2).
An exact proof term for the current goal is (andER (a = (a1,a2) ∧ x = (x1,x2)) (Rlt a1 x1 ∨ (a1 = x1 ∧ Rlt a2 x2)) Hcore1).
Apply Hex2 to the current goal.
Let y1 be given.
Assume Hy1pack.
Apply Hy1pack to the current goal.
Let y2 be given.
Assume Hy2pack.
Apply Hy2pack to the current goal.
Let b1 be given.
Assume Hb1pack.
Apply Hb1pack to the current goal.
Let b2 be given.
Assume Hcore2.
We prove the intermediate claim Hxb: x = (y1,y2) ∧ b = (b1,b2).
An exact proof term for the current goal is (andEL (x = (y1,y2) ∧ b = (b1,b2)) (Rlt y1 b1 ∨ (y1 = b1 ∧ Rlt y2 b2)) Hcore2).
We prove the intermediate claim Hx_eq2: x = (y1,y2).
An exact proof term for the current goal is (andEL (x = (y1,y2)) (b = (b1,b2)) Hxb).
We prove the intermediate claim Hb_eq: b = (b1,b2).
An exact proof term for the current goal is (andER (x = (y1,y2)) (b = (b1,b2)) Hxb).
We prove the intermediate claim Hlex2: Rlt y1 b1 ∨ (y1 = b1 ∧ Rlt y2 b2).
An exact proof term for the current goal is (andER (x = (y1,y2) ∧ b = (b1,b2)) (Rlt y1 b1 ∨ (y1 = b1 ∧ Rlt y2 b2)) Hcore2).
We prove the intermediate claim HaDef: a = (eps_ 1,eps_ 1).
Use reflexivity.
We prove the intermediate claim HbDef: b = (eps_ 1,1).
Use reflexivity.
We prove the intermediate claim Ha0: a 0 = eps_ 1.
rewrite the current goal using HaDef (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) (eps_ 1)).
We prove the intermediate claim Ha1: a 1 = eps_ 1.
rewrite the current goal using HaDef (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq (eps_ 1) (eps_ 1)).
We prove the intermediate claim Hb0: b 0 = eps_ 1.
rewrite the current goal using HbDef (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) 1).
We prove the intermediate claim Hb1: b 1 = 1.
rewrite the current goal using HbDef (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq (eps_ 1) 1).
We prove the intermediate claim Ha0a1: a 0 = a1.
rewrite the current goal using Ha_eq (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq a1 a2).
We prove the intermediate claim Ha1a2: a 1 = a2.
rewrite the current goal using Ha_eq (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq a1 a2).
We prove the intermediate claim Hb0b1: b 0 = b1.
rewrite the current goal using Hb_eq (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq b1 b2).
We prove the intermediate claim Hb1b2: b 1 = b2.
rewrite the current goal using Hb_eq (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq b1 b2).
We prove the intermediate claim Ha1eq: a1 = eps_ 1.
rewrite the current goal using Ha0a1 (from right to left).
An exact proof term for the current goal is Ha0.
We prove the intermediate claim Ha2eq: a2 = eps_ 1.
rewrite the current goal using Ha1a2 (from right to left).
An exact proof term for the current goal is Ha1.
We prove the intermediate claim Hb1eq: b1 = eps_ 1.
rewrite the current goal using Hb0b1 (from right to left).
An exact proof term for the current goal is Hb0.
We prove the intermediate claim Hb2eq: b2 = 1.
rewrite the current goal using Hb1b2 (from right to left).
An exact proof term for the current goal is Hb1.
We prove the intermediate claim Hx1eq0: x 0 = x1.
rewrite the current goal using Hx_eq (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq x1 x2).
We prove the intermediate claim Hx1eq1: x 1 = x2.
rewrite the current goal using Hx_eq (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq x1 x2).
We prove the intermediate claim Hy1eq0: x 0 = y1.
rewrite the current goal using Hx_eq2 (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq y1 y2).
We prove the intermediate claim Hy1eq1: x 1 = y2.
rewrite the current goal using Hx_eq2 (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq y1 y2).
We prove the intermediate claim Hx1y1: x1 = y1.
rewrite the current goal using Hx1eq0 (from right to left).
rewrite the current goal using Hy1eq0 (from right to left).
Use reflexivity.
We prove the intermediate claim Hx2y2: x2 = y2.
rewrite the current goal using Hx1eq1 (from right to left).
rewrite the current goal using Hy1eq1 (from right to left).
Use reflexivity.
We prove the intermediate claim Hx1eq: x1 = eps_ 1.
We prove the intermediate claim Hnotlt: ¬ (Rlt x1 (eps_ 1)).
Apply (Hlex1 (¬ (Rlt x1 (eps_ 1)))) to the current goal.
Assume Hlt: Rlt a1 x1.
We prove the intermediate claim Hepslt: Rlt (eps_ 1) x1.
rewrite the current goal using Ha1eq (from right to left).
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is (not_Rlt_sym (eps_ 1) x1 Hepslt).
Assume Hpair.
We prove the intermediate claim Ha1x1: a1 = x1.
An exact proof term for the current goal is (andEL (a1 = x1) (Rlt a2 x2) Hpair).
We prove the intermediate claim Hx1eps: x1 = eps_ 1.
rewrite the current goal using Ha1x1 (from right to left).
An exact proof term for the current goal is Ha1eq.
Assume Hbad: Rlt x1 (eps_ 1).
We prove the intermediate claim Hbad2: Rlt (eps_ 1) (eps_ 1).
rewrite the current goal using Hx1eps (from right to left) at position 1.
An exact proof term for the current goal is Hbad.
An exact proof term for the current goal is ((not_Rlt_refl (eps_ 1) eps_1_in_R) Hbad2).
Apply (Hlex2 (x1 = eps_ 1)) to the current goal.
Assume Hy1lt: Rlt y1 b1.
Apply FalseE to the current goal.
We prove the intermediate claim Hy1lt2: Rlt x1 (eps_ 1).
rewrite the current goal using Hx1y1 (from left to right).
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hy1lt.
An exact proof term for the current goal is (Hnotlt Hy1lt2).
Assume Hpair2.
We prove the intermediate claim Hy1b1: y1 = b1.
An exact proof term for the current goal is (andEL (y1 = b1) (Rlt y2 b2) Hpair2).
rewrite the current goal using Hx1y1 (from left to right).
rewrite the current goal using Hy1b1 (from left to right).
An exact proof term for the current goal is Hb1eq.
We prove the intermediate claim Hx1eps: x 0 = eps_ 1.
rewrite the current goal using Hx1eq0 (from left to right).
An exact proof term for the current goal is Hx1eq.
We prove the intermediate claim Hx2lt1: Rlt x2 1.
We prove the intermediate claim Hy1eqb1: y1 = b1.
rewrite the current goal using Hx1y1 (from right to left).
rewrite the current goal using Hx1eq (from left to right).
rewrite the current goal using Hb1eq (from right to left).
Use reflexivity.
We prove the intermediate claim Hb1R: b1 ∈ R.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is eps_1_in_R.
Apply (Hlex2 (Rlt x2 1)) to the current goal.
Assume Hy1lt: Rlt y1 b1.
Apply FalseE to the current goal.
We prove the intermediate claim Hbad: Rlt b1 b1.
rewrite the current goal using Hy1eqb1 (from right to left) at position 1.
An exact proof term for the current goal is Hy1lt.
An exact proof term for the current goal is ((not_Rlt_refl b1 Hb1R) Hbad).
Assume Hpair.
We prove the intermediate claim Hy2b2: Rlt y2 b2.
An exact proof term for the current goal is (andER (y1 = b1) (Rlt y2 b2) Hpair).
rewrite the current goal using Hx2y2 (from left to right) at position 1.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hy2b2.
We prove the intermediate claim Hx2R: x2 ∈ R.
An exact proof term for the current goal is (RltE_left x2 1 Hx2lt1).
We prove the intermediate claim Hepsltx2: Rlt (eps_ 1) x2.
Apply (Hlex1 (Rlt (eps_ 1) x2)) to the current goal.
Assume Hlt: Rlt a1 x1.
Apply FalseE to the current goal.
We prove the intermediate claim Hbad: Rlt (eps_ 1) (eps_ 1).
rewrite the current goal using Ha1eq (from right to left) at position 1.
rewrite the current goal using Hx1eq (from right to left).
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is ((not_Rlt_refl (eps_ 1) eps_1_in_R) Hbad).
Assume Hpair.
We prove the intermediate claim Ha2x2: Rlt a2 x2.
An exact proof term for the current goal is (andER (a1 = x1) (Rlt a2 x2) Hpair).
rewrite the current goal using Ha2eq (from right to left) at position 1.
An exact proof term for the current goal is Ha2x2.
We prove the intermediate claim Hx2UI: x2 ∈ unit_interval.
We prove the intermediate claim H0ltx2: Rlt 0 x2.
An exact proof term for the current goal is (Rlt_tra 0 (eps_ 1) x2 eps_1_pos_R Hepsltx2).
We prove the intermediate claim Hnltx20: ¬ (Rlt x2 0).
An exact proof term for the current goal is (not_Rlt_sym 0 x2 H0ltx2).
We prove the intermediate claim Hnlt1x2: ¬ (Rlt 1 x2).
An exact proof term for the current goal is (not_Rlt_sym x2 1 Hx2lt1).
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z 0) ∧ ¬ (Rlt 1 z)) x2 Hx2R (andI (¬ (Rlt x2 0)) (¬ (Rlt 1 x2)) Hnltx20 Hnlt1x2)).
We prove the intermediate claim HxOrdSq: x ∈ ordered_square.
We prove the intermediate claim Hsqdef: ordered_square = setprod unit_interval unit_interval.
Use reflexivity.
rewrite the current goal using Hsqdef (from left to right).
We prove the intermediate claim Hx1UI: x1 ∈ unit_interval.
rewrite the current goal using Hx1eq (from left to right).
An exact proof term for the current goal is eps_1_in_unit_interval.
rewrite the current goal using Hx_eq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval x1 x2 Hx1UI Hx2UI).
We prove the intermediate claim Hstripdef: ordered_square_open_strip = {p0 ∈ ordered_square|∃y : set, p0 = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)}.
Use reflexivity.
rewrite the current goal using Hstripdef (from left to right).
Apply (SepI ordered_square (λp0 : set ⇒ ∃y : set, p0 = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)) x HxOrdSq) to the current goal.
We use x2 to witness the existential quantifier.
We will prove x = (eps_ 1,x2) ∧ Rlt (eps_ 1) x2 ∧ ¬ (Rlt 1 x2).
Apply andI to the current goal.
Apply andI to the current goal.
rewrite the current goal using Hx_eq (from left to right).
rewrite the current goal using Hx1eq (from left to right).
Use reflexivity.
An exact proof term for the current goal is Hepsltx2.
An exact proof term for the current goal is (not_Rlt_sym x2 1 Hx2lt1).
We prove the intermediate claim HWinComp: W ∩ (X ∖ A) = Empty.
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume Hx: x ∈ W ∩ (X ∖ A).
We will prove x ∈ Empty.
We prove the intermediate claim HxW: x ∈ W.
An exact proof term for the current goal is (binintersectE1 W (X ∖ A) x Hx).
We prove the intermediate claim HxComp: x ∈ X ∖ A.
An exact proof term for the current goal is (binintersectE2 W (X ∖ A) x Hx).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (HWsubA x HxW).
We prove the intermediate claim HxnotA: x ∉ A.
An exact proof term for the current goal is (setminusE2 X A x HxComp).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotA HxA).
We prove the intermediate claim Hbad: W ∩ (X ∖ A) ≠ Empty.
An exact proof term for the current goal is (Hpcond W HWopen HpW).
An exact proof term for the current goal is (Hbad HWinComp).
We prove the intermediate claim Hpbd_dic: p ∈ boundary_of X R2_dictionary_order_topology A.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hpbd_std.
An exact proof term for the current goal is (Hpnot_bd_dic Hpbd_dic).
∎