We will prove ordered_square_topology ≠ subspace_topology (setprod R R) R2_dictionary_order_topology ordered_square.
Assume Heq: ordered_square_topology = subspace_topology (setprod R R) R2_dictionary_order_topology ordered_square.
We will prove False.
Set U to be the term ordered_square_open_strip.
We prove the intermediate claim HUdic: U ∈ subspace_topology (setprod R R) R2_dictionary_order_topology ordered_square.
We prove the intermediate claim HUsub: U ⊆ ordered_square.
Let p be given.
Assume Hp: p ∈ U.
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)) p Hp).
We prove the intermediate claim HUpow: U ∈ 𝒫 ordered_square.
An exact proof term for the current goal is (PowerI ordered_square U HUsub).
Set a to be the term (eps_ 1,eps_ 1).
Set b to be the term (eps_ 1,2).
Set V to be the term {p ∈ setprod R R|order_rel (setprod R R) a p ∧ order_rel (setprod R R) p b}.
We prove the intermediate claim HVopen: V ∈ R2_dictionary_order_topology.
Set X to be the term setprod R R.
We prove the intermediate claim HS: subbasis_on X (open_rays_subbasis X).
An exact proof term for the current goal is (open_rays_subbasis_is_subbasis X).
We prove the intermediate claim HT: 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 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) 2 eps_1_in_R two_in_R).
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 HS 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 HS HU2S).
We prove the intermediate claim HVeq: V = U1 ∩ U2.
We prove the intermediate claim HdefV: V = {p ∈ X|order_rel X a p ∧ order_rel X p b}.
Use reflexivity.
rewrite the current goal using HdefV (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 HVeq (from left to right).
An exact proof term for the current goal is (topology_binintersect_closed X R2_dictionary_order_topology U1 U2 HT HU1open HU2open).
We prove the intermediate claim HeqU: U = V ∩ ordered_square.
Apply set_ext to the current goal.
Let p be given.
Assume HpU: p ∈ U.
We will prove p ∈ V ∩ ordered_square.
We prove the intermediate claim HpSq: p ∈ ordered_square.
An exact proof term for the current goal is (HUsub p HpU).
We prove the intermediate claim Hexy: ∃y : set, p = (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)) p HpU).
Apply Hexy to the current goal.
Let y be given.
Assume Hyprop.
We prove the intermediate claim Hpair: (p = (eps_ 1,y) ∧ Rlt (eps_ 1) y).
An exact proof term for the current goal is (andEL (p = (eps_ 1,y) ∧ Rlt (eps_ 1) y) (¬ (Rlt 1 y)) Hyprop).
We prove the intermediate claim Hpy: p = (eps_ 1,y).
An exact proof term for the current goal is (andEL (p = (eps_ 1,y)) (Rlt (eps_ 1) y) Hpair).
We prove the intermediate claim Hey: Rlt (eps_ 1) y.
An exact proof term for the current goal is (andER (p = (eps_ 1,y)) (Rlt (eps_ 1) y) Hpair).
We prove the intermediate claim Hnlt1y: ¬ (Rlt 1 y).
An exact proof term for the current goal is (andER (p = (eps_ 1,y) ∧ Rlt (eps_ 1) y) (¬ (Rlt 1 y)) Hyprop).
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (RltE_right (eps_ 1) y Hey).
We prove the intermediate claim Hylt2: Rlt y 2.
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim H1S: SNo 1.
An exact proof term for the current goal is (real_SNo 1 real_1).
We prove the intermediate claim H2S: SNo 2.
An exact proof term for the current goal is (real_SNo 2 two_in_R).
We prove the intermediate claim HnltS: ¬ (1 < y).
Assume Hlt: 1 < y.
We prove the intermediate claim H1y: Rlt 1 y.
An exact proof term for the current goal is (RltI 1 y real_1 HyR Hlt).
An exact proof term for the current goal is (Hnlt1y H1y).
Apply (SNoLt_trichotomy_or_impred y 1 HyS H1S (Rlt y 2)) to the current goal.
Assume Hylt1S: y < 1.
We prove the intermediate claim Hylt2S: y < 2.
An exact proof term for the current goal is (SNoLt_tra y 1 2 HyS H1S H2S Hylt1S SNoLt_1_2).
An exact proof term for the current goal is (RltI y 2 HyR two_in_R Hylt2S).
Assume Hyeq: y = 1.
rewrite the current goal using Hyeq (from left to right).
An exact proof term for the current goal is (RltI 1 2 real_1 two_in_R SNoLt_1_2).
Assume H1ltyS: 1 < y.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnltS H1ltyS).
We prove the intermediate claim HpV: p ∈ V.
rewrite the current goal using Hpy (from left to right).
We prove the intermediate claim HpRR: (eps_ 1,y) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (eps_ 1) y eps_1_in_R HyR).
We prove the intermediate claim Hord1: order_rel (setprod R R) a (eps_ 1,y).
Apply (order_rel_setprod_R_R_intro (eps_ 1) (eps_ 1) (eps_ 1) y) to the current goal.
Apply orIR to the current goal.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is Hey.
We prove the intermediate claim Hord2: order_rel (setprod R R) (eps_ 1,y) b.
Apply (order_rel_setprod_R_R_intro (eps_ 1) y (eps_ 1) 2) to the current goal.
Apply orIR to the current goal.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is Hylt2.
We prove the intermediate claim Hpconj: order_rel (setprod R R) a (eps_ 1,y) ∧ order_rel (setprod R R) (eps_ 1,y) b.
An exact proof term for the current goal is (andI (order_rel (setprod R R) a (eps_ 1,y)) (order_rel (setprod R R) (eps_ 1,y) b) Hord1 Hord2).
An exact proof term for the current goal is (SepI (setprod R R) (λp0 : set ⇒ order_rel (setprod R R) a p0 ∧ order_rel (setprod R R) p0 b) (eps_ 1,y) HpRR Hpconj).
Apply binintersectI to the current goal.
An exact proof term for the current goal is HpV.
An exact proof term for the current goal is HpSq.
Let p be given.
Assume HpCap: p ∈ V ∩ ordered_square.
We will prove p ∈ U.
We prove the intermediate claim HpV: p ∈ V.
An exact proof term for the current goal is (binintersectE1 V ordered_square p HpCap).
We prove the intermediate claim HpSq: p ∈ ordered_square.
An exact proof term for the current goal is (binintersectE2 V ordered_square p HpCap).
We prove the intermediate claim HpRR: p ∈ setprod R R.
An exact proof term for the current goal is (SepE1 (setprod R R) (λp0 : set ⇒ order_rel (setprod R R) a p0 ∧ order_rel (setprod R R) p0 b) p HpV).
We prove the intermediate claim HpEta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta R R p HpRR).
We prove the intermediate claim Hpord: order_rel (setprod R R) a p ∧ order_rel (setprod R R) p b.
An exact proof term for the current goal is (SepE2 (setprod R R) (λp0 : set ⇒ order_rel (setprod R R) a p0 ∧ order_rel (setprod R R) p0 b) p HpV).
We prove the intermediate claim Hord1: order_rel (setprod R R) a p.
An exact proof term for the current goal is (andEL (order_rel (setprod R R) a p) (order_rel (setprod R R) p b) Hpord).
We prove the intermediate claim Hord2: order_rel (setprod R R) p b.
An exact proof term for the current goal is (andER (order_rel (setprod R R) a p) (order_rel (setprod R R) p b) Hpord).
We prove the intermediate claim Hex_ap: ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ p = (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 p Hord1).
We prove the intermediate claim Hex_pb: ∃a1 a2 b1 b2 : set, p = (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 p b Hord2).
We prove the intermediate claim Hdisj1p: Rlt (eps_ 1) (p 0) ∨ ((eps_ 1) = (p 0) ∧ Rlt (eps_ 1) (p 1)).
Apply Hex_ap to the current goal.
Let a1 be given.
Assume Hex_a2.
Apply Hex_a2 to the current goal.
Let a2 be given.
Assume Hex_b1.
Apply Hex_b1 to the current goal.
Let b1 be given.
Assume Hex_b2.
Apply Hex_b2 to the current goal.
Let b2 be given.
Assume Hap.
We prove the intermediate claim Hcore1: a = (a1,a2) ∧ p = (b1,b2).
An exact proof term for the current goal is (andEL (a = (a1,a2) ∧ p = (b1,b2)) (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)) Hap).
We prove the intermediate claim HaEq: a = (a1,a2).
An exact proof term for the current goal is (andEL (a = (a1,a2)) (p = (b1,b2)) Hcore1).
We prove the intermediate claim HpEq: p = (b1,b2).
An exact proof term for the current goal is (andER (a = (a1,a2)) (p = (b1,b2)) Hcore1).
We prove the intermediate claim Hdisj1: Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2).
An exact proof term for the current goal is (andER (a = (a1,a2) ∧ p = (b1,b2)) (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)) Hap).
We prove the intermediate claim HaDef: a = (eps_ 1,eps_ 1).
Use reflexivity.
We prove the intermediate claim Haa: (eps_ 1,eps_ 1) = (a1,a2).
rewrite the current goal using HaDef (from left to right) at position 1.
An exact proof term for the current goal is HaEq.
We prove the intermediate claim HaCoords: (eps_ 1) = a1 ∧ (eps_ 1) = a2.
An exact proof term for the current goal is (tuple_eq_coords (eps_ 1) (eps_ 1) a1 a2 Haa).
We prove the intermediate claim Ha1eq: a1 = eps_ 1.
Use symmetry.
An exact proof term for the current goal is (andEL ((eps_ 1) = a1) ((eps_ 1) = a2) HaCoords).
We prove the intermediate claim Ha2eq: a2 = eps_ 1.
Use symmetry.
An exact proof term for the current goal is (andER ((eps_ 1) = a1) ((eps_ 1) = a2) HaCoords).
We prove the intermediate claim Hbb: (b1,b2) = (p 0,p 1).
rewrite the current goal using HpEq (from right to left) at position 1.
An exact proof term for the current goal is HpEta.
We prove the intermediate claim HbCoords: b1 = p 0 ∧ b2 = p 1.
An exact proof term for the current goal is (tuple_eq_coords b1 b2 (p 0) (p 1) Hbb).
We prove the intermediate claim Hb1eq: b1 = p 0.
An exact proof term for the current goal is (andEL (b1 = p 0) (b2 = p 1) HbCoords).
We prove the intermediate claim Hb2eq: b2 = p 1.
An exact proof term for the current goal is (andER (b1 = p 0) (b2 = p 1) HbCoords).
Apply (Hdisj1 (Rlt (eps_ 1) (p 0) ∨ ((eps_ 1) = (p 0) ∧ Rlt (eps_ 1) (p 1)))) to the current goal.
Assume Hlt: Rlt a1 b1.
Apply orIL to the current goal.
We will prove Rlt (eps_ 1) (p 0).
We prove the intermediate claim Htmp: Rlt (eps_ 1) b1.
rewrite the current goal using Ha1eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
rewrite the current goal using Hb1eq (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
Assume Hc: a1 = b1 ∧ Rlt a2 b2.
We prove the intermediate claim Ha1b1: a1 = b1.
An exact proof term for the current goal is (andEL (a1 = b1) (Rlt a2 b2) Hc).
We prove the intermediate claim Ha2b2: Rlt a2 b2.
An exact proof term for the current goal is (andER (a1 = b1) (Rlt a2 b2) Hc).
We prove the intermediate claim Heq0: (eps_ 1) = (p 0).
We will prove (eps_ 1) = (p 0).
We prove the intermediate claim Heq1: (eps_ 1) = b1.
rewrite the current goal using Ha1eq (from right to left) at position 1.
An exact proof term for the current goal is Ha1b1.
rewrite the current goal using Hb1eq (from right to left) at position 1.
An exact proof term for the current goal is Heq1.
We prove the intermediate claim Hlt1: Rlt (eps_ 1) (p 1).
We will prove Rlt (eps_ 1) (p 1).
We prove the intermediate claim Htmp2: Rlt (eps_ 1) b2.
rewrite the current goal using Ha2eq (from right to left) at position 1.
An exact proof term for the current goal is Ha2b2.
rewrite the current goal using Hb2eq (from right to left) at position 1.
An exact proof term for the current goal is Htmp2.
Apply orIR to the current goal.
An exact proof term for the current goal is (andI ((eps_ 1) = (p 0)) (Rlt (eps_ 1) (p 1)) Heq0 Hlt1).
We prove the intermediate claim Hdisj2p: Rlt (p 0) (eps_ 1) ∨ ((p 0) = (eps_ 1) ∧ Rlt (p 1) 2).
Apply Hex_pb to the current goal.
Let c1 be given.
Assume Hex_c2.
Apply Hex_c2 to the current goal.
Let c2 be given.
Assume Hex_d1.
Apply Hex_d1 to the current goal.
Let d1 be given.
Assume Hex_d2.
Apply Hex_d2 to the current goal.
Let d2 be given.
Assume Hpb.
We prove the intermediate claim Hcore2: p = (c1,c2) ∧ b = (d1,d2).
An exact proof term for the current goal is (andEL (p = (c1,c2) ∧ b = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hpb).
We prove the intermediate claim HpEq2: p = (c1,c2).
An exact proof term for the current goal is (andEL (p = (c1,c2)) (b = (d1,d2)) Hcore2).
We prove the intermediate claim HbEq: b = (d1,d2).
An exact proof term for the current goal is (andER (p = (c1,c2)) (b = (d1,d2)) Hcore2).
We prove the intermediate claim Hdisj2: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).
An exact proof term for the current goal is (andER (p = (c1,c2) ∧ b = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hpb).
We prove the intermediate claim Hpc: (c1,c2) = (p 0,p 1).
rewrite the current goal using HpEq2 (from right to left) at position 1.
An exact proof term for the current goal is HpEta.
We prove the intermediate claim HpCoords: c1 = p 0 ∧ c2 = p 1.
An exact proof term for the current goal is (tuple_eq_coords c1 c2 (p 0) (p 1) Hpc).
We prove the intermediate claim Hc1eq: c1 = p 0.
An exact proof term for the current goal is (andEL (c1 = p 0) (c2 = p 1) HpCoords).
We prove the intermediate claim Hc2eq: c2 = p 1.
An exact proof term for the current goal is (andER (c1 = p 0) (c2 = p 1) HpCoords).
We prove the intermediate claim HbDef: b = (eps_ 1,2).
Use reflexivity.
We prove the intermediate claim Hbd: (eps_ 1,2) = (d1,d2).
rewrite the current goal using HbDef (from left to right) at position 1.
An exact proof term for the current goal is HbEq.
We prove the intermediate claim HbCoords: (eps_ 1) = d1 ∧ 2 = d2.
An exact proof term for the current goal is (tuple_eq_coords (eps_ 1) 2 d1 d2 Hbd).
We prove the intermediate claim Hd1eq: d1 = eps_ 1.
Use symmetry.
An exact proof term for the current goal is (andEL ((eps_ 1) = d1) (2 = d2) HbCoords).
We prove the intermediate claim Hd2eq: d2 = 2.
Use symmetry.
An exact proof term for the current goal is (andER ((eps_ 1) = d1) (2 = d2) HbCoords).
Apply (Hdisj2 (Rlt (p 0) (eps_ 1) ∨ ((p 0) = (eps_ 1) ∧ Rlt (p 1) 2))) to the current goal.
Assume Hlt: Rlt c1 d1.
Apply orIL to the current goal.
We will prove Rlt (p 0) (eps_ 1).
We prove the intermediate claim Htmp: Rlt (p 0) d1.
rewrite the current goal using Hc1eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
rewrite the current goal using Hd1eq (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
Assume Hc: c1 = d1 ∧ Rlt c2 d2.
We prove the intermediate claim Hc1d1: c1 = d1.
An exact proof term for the current goal is (andEL (c1 = d1) (Rlt c2 d2) Hc).
We prove the intermediate claim Hc2d2: Rlt c2 d2.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Hc).
We prove the intermediate claim Heq0: (p 0) = (eps_ 1).
We will prove (p 0) = (eps_ 1).
We prove the intermediate claim Heq1: (p 0) = d1.
rewrite the current goal using Hc1eq (from right to left) at position 1.
An exact proof term for the current goal is Hc1d1.
rewrite the current goal using Hd1eq (from right to left) at position 1.
An exact proof term for the current goal is Heq1.
We prove the intermediate claim Hlt1: Rlt (p 1) 2.
We will prove Rlt (p 1) 2.
We prove the intermediate claim Htmp2: Rlt (p 1) d2.
rewrite the current goal using Hc2eq (from right to left) at position 1.
An exact proof term for the current goal is Hc2d2.
rewrite the current goal using Hd2eq (from right to left) at position 1.
An exact proof term for the current goal is Htmp2.
Apply orIR to the current goal.
An exact proof term for the current goal is (andI ((p 0) = (eps_ 1)) (Rlt (p 1) 2) Heq0 Hlt1).
We prove the intermediate claim Hp0eq: (p 0) = (eps_ 1).
Apply (Hdisj2p ((p 0) = (eps_ 1))) to the current goal.
Assume Hp0lt: Rlt (p 0) (eps_ 1).
Apply FalseE to the current goal.
Apply (Hdisj1p False) to the current goal.
Assume Hepslt: Rlt (eps_ 1) (p 0).
An exact proof term for the current goal is ((not_Rlt_sym (eps_ 1) (p 0) Hepslt) Hp0lt).
Assume Hc: (eps_ 1) = (p 0) ∧ Rlt (eps_ 1) (p 1).
We prove the intermediate claim Heq: (p 0) = (eps_ 1).
Use symmetry.
An exact proof term for the current goal is (andEL ((eps_ 1) = (p 0)) (Rlt (eps_ 1) (p 1)) Hc).
We prove the intermediate claim Hbad: Rlt (eps_ 1) (eps_ 1).
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hp0lt.
An exact proof term for the current goal is ((not_Rlt_refl (eps_ 1) eps_1_in_R) Hbad).
Assume Hc: (p 0) = (eps_ 1) ∧ Rlt (p 1) 2.
An exact proof term for the current goal is (andEL ((p 0) = (eps_ 1)) (Rlt (p 1) 2) Hc).
We prove the intermediate claim Hey: Rlt (eps_ 1) (p 1).
Apply (Hdisj1p (Rlt (eps_ 1) (p 1))) to the current goal.
Assume Hepslt: Rlt (eps_ 1) (p 0).
Apply FalseE to the current goal.
We prove the intermediate claim Hbad: Rlt (eps_ 1) (eps_ 1).
rewrite the current goal using Hp0eq (from right to left) at position 2.
An exact proof term for the current goal is Hepslt.
An exact proof term for the current goal is ((not_Rlt_refl (eps_ 1) eps_1_in_R) Hbad).
Assume Hc: (eps_ 1) = (p 0) ∧ Rlt (eps_ 1) (p 1).
An exact proof term for the current goal is (andER ((eps_ 1) = (p 0)) (Rlt (eps_ 1) (p 1)) Hc).
We prove the intermediate claim HyU: (p 1) ∈ unit_interval.
An exact proof term for the current goal is (ap1_Sigma unit_interval (λ_ : set ⇒ unit_interval) p HpSq).
We prove the intermediate claim Hnlt1y: ¬ (Rlt 1 (p 1)).
An exact proof term for the current goal is (andER (¬ (Rlt (p 1) 0)) (¬ (Rlt 1 (p 1))) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (p 1) HyU)).
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 (p 1) to witness the existential quantifier.
We will prove p = (eps_ 1,p 1) ∧ Rlt (eps_ 1) (p 1) ∧ ¬ (Rlt 1 (p 1)).
Apply andI to the current goal.
We will prove p = (eps_ 1,p 1) ∧ Rlt (eps_ 1) (p 1).
Apply andI to the current goal.
We will prove p = (eps_ 1,p 1).
rewrite the current goal using HpEta (from left to right) at position 1.
rewrite the current goal using Hp0eq (from left to right).
Use reflexivity.
An exact proof term for the current goal is Hey.
An exact proof term for the current goal is Hnlt1y.
We prove the intermediate claim Hex: ∃W ∈ R2_dictionary_order_topology, U = W ∩ ordered_square.
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HVopen.
An exact proof term for the current goal is HeqU.
An exact proof term for the current goal is (SepI (𝒫 ordered_square) (λU0 : set ⇒ ∃W ∈ R2_dictionary_order_topology, U0 = W ∩ ordered_square) U HUpow Hex).
We prove the intermediate claim HUord: U ∈ ordered_square_topology.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HUdic.
We prove the intermediate claim HUnord: ¬ (U ∈ ordered_square_topology).
Assume HU: U ∈ ordered_square_topology.
We will prove False.
We prove the intermediate claim HUgt: U ∈ generated_topology ordered_square ordered_square_order_basis.
We prove the intermediate claim HdefT: ordered_square_topology = generated_topology ordered_square ordered_square_order_basis.
Use reflexivity.
rewrite the current goal using HdefT (from right to left).
An exact proof term for the current goal is HU.
We prove the intermediate claim HUpoint: ∀x ∈ U, ∃I ∈ ordered_square_order_basis, x ∈ I ∧ I ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 ordered_square) (λU0 : set ⇒ ∀x ∈ U0, ∃b0 ∈ ordered_square_order_basis, x ∈ b0 ∧ b0 ⊆ U0) U HUgt).
Set p0 to be the term (eps_ 1,1).
We prove the intermediate claim Hp0Sq: p0 ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval (eps_ 1) 1 eps_1_in_unit_interval one_in_unit_interval).
We prove the intermediate claim Hp0U: p0 ∈ U.
Apply (SepI ordered_square (λp : set ⇒ ∃y : set, p = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)) p0 Hp0Sq) to the current goal.
We use 1 to witness the existential quantifier.
We will prove p0 = (eps_ 1,1) ∧ Rlt (eps_ 1) 1 ∧ ¬ (Rlt 1 1).
Apply andI to the current goal.
We will prove p0 = (eps_ 1,1) ∧ Rlt (eps_ 1) 1.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is eps_1_lt1_R.
An exact proof term for the current goal is (not_Rlt_refl 1 real_1).
We prove the intermediate claim HexI: ∃I ∈ ordered_square_order_basis, p0 ∈ I ∧ I ⊆ U.
An exact proof term for the current goal is (HUpoint p0 Hp0U).
Apply HexI to the current goal.
Let I be given.
Assume HIprop.
Apply HIprop to the current goal.
Assume HIbas HIcore.
Apply HIcore to the current goal.
Assume Hp0I HIU.
Set Bint to be the term {J ∈ 𝒫 ordered_square|∃a ∈ ordered_square, ∃b ∈ ordered_square, J = {x ∈ ordered_square|order_rel (setprod R R) a x ∧ order_rel (setprod R R) x b}}.
Set Blow to be the term {J ∈ 𝒫 ordered_square|∃b ∈ ordered_square, J = {x ∈ ordered_square|order_rel (setprod R R) x b}}.
Set Bup to be the term {J ∈ 𝒫 ordered_square|∃a ∈ ordered_square, J = {x ∈ ordered_square|order_rel (setprod R R) a x}}.
We prove the intermediate claim HIcase: I ∈ ((Bint ∪ Blow) ∪ Bup).
We prove the intermediate claim Hdef: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).
Use reflexivity.
rewrite the current goal using Hdef (from right to left).
An exact proof term for the current goal is HIbas.
Apply (binunionE (Bint ∪ Blow) Bup I HIcase) to the current goal.
Assume HIleft: I ∈ (Bint ∪ Blow).
Apply (binunionE Bint Blow I HIleft) to the current goal.
Assume HIint: I ∈ Bint.
We prove the intermediate claim HIint_ex: ∃a ∈ ordered_square, ∃b ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) a x ∧ order_rel (setprod R R) x b}.
An exact proof term for the current goal is (SepE2 (𝒫 ordered_square) (λJ0 : set ⇒ ∃a ∈ ordered_square, ∃b ∈ ordered_square, J0 = {x ∈ ordered_square|order_rel (setprod R R) a x ∧ order_rel (setprod R R) x b}) I HIint).
Apply HIint_ex to the current goal.
Let a be given.
Assume Ha_prop.
Apply Ha_prop to the current goal.
Assume HaSq Hexb.
Apply Hexb to the current goal.
Let b be given.
Assume Hb_prop.
Apply Hb_prop to the current goal.
Assume HbSq HeqI.
We prove the intermediate claim Hp0I': p0 ∈ {x ∈ ordered_square|order_rel (setprod R R) a x ∧ order_rel (setprod R R) x b}.
rewrite the current goal using HeqI (from right to left).
An exact proof term for the current goal is Hp0I.
We prove the intermediate claim Hp0ord: order_rel (setprod R R) a p0 ∧ order_rel (setprod R R) p0 b.
An exact proof term for the current goal is (SepE2 ordered_square (λx : set ⇒ order_rel (setprod R R) a x ∧ order_rel (setprod R R) x b) p0 Hp0I').
We prove the intermediate claim Hord2: order_rel (setprod R R) p0 b.
An exact proof term for the current goal is (andER (order_rel (setprod R R) a p0) (order_rel (setprod R R) p0 b) Hp0ord).
We prove the intermediate claim HbEta: b = (b 0,b 1).
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval b HbSq).
We prove the intermediate claim Hb0U: (b 0) ∈ unit_interval.
An exact proof term for the current goal is (ap0_Sigma unit_interval (λ_ : set ⇒ unit_interval) b HbSq).
We prove the intermediate claim Hb1U: (b 1) ∈ unit_interval.
An exact proof term for the current goal is (ap1_Sigma unit_interval (λ_ : set ⇒ unit_interval) b HbSq).
We prove the intermediate claim Hb0R: (b 0) ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (b 0) Hb0U).
We prove the intermediate claim Hb0prop: ¬ (Rlt 1 (b 0)).
An exact proof term for the current goal is (andER (¬ (Rlt (b 0) 0)) (¬ (Rlt 1 (b 0))) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (b 0) Hb0U)).
We prove the intermediate claim Hb1prop: ¬ (Rlt 1 (b 1)).
An exact proof term for the current goal is (andER (¬ (Rlt (b 1) 0)) (¬ (Rlt 1 (b 1))) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (b 1) Hb1U)).
We prove the intermediate claim Hepsltb0: Rlt (eps_ 1) (b 0).
We prove the intermediate claim Hex_pb: ∃c1 c2 d1 d2 : set, p0 = (c1,c2) ∧ b = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).
An exact proof term for the current goal is (order_rel_setprod_R_R_unfold p0 b Hord2).
Apply Hex_pb to the current goal.
Let c1 be given.
Assume Hc2.
Apply Hc2 to the current goal.
Let c2 be given.
Assume Hd1.
Apply Hd1 to the current goal.
Let d1 be given.
Assume Hd2.
Apply Hd2 to the current goal.
Let d2 be given.
Assume Hcore.
We prove the intermediate claim Hpb: p0 = (c1,c2) ∧ b = (d1,d2).
An exact proof term for the current goal is (andEL (p0 = (c1,c2) ∧ b = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim Hp0Eq: p0 = (c1,c2).
An exact proof term for the current goal is (andEL (p0 = (c1,c2)) (b = (d1,d2)) Hpb).
We prove the intermediate claim HbEq: b = (d1,d2).
An exact proof term for the current goal is (andER (p0 = (c1,c2)) (b = (d1,d2)) Hpb).
We prove the intermediate claim Hdisj: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).
An exact proof term for the current goal is (andER (p0 = (c1,c2) ∧ b = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim Hp0def: p0 = (eps_ 1,1).
Use reflexivity.
We prove the intermediate claim Hp0c: (eps_ 1,1) = (c1,c2).
rewrite the current goal using Hp0def (from left to right) at position 1.
An exact proof term for the current goal is Hp0Eq.
We prove the intermediate claim Hp0coords: (eps_ 1) = c1 ∧ 1 = c2.
An exact proof term for the current goal is (tuple_eq_coords (eps_ 1) 1 c1 c2 Hp0c).
We prove the intermediate claim Hc1eq: c1 = eps_ 1.
Use symmetry.
An exact proof term for the current goal is (andEL ((eps_ 1) = c1) (1 = c2) Hp0coords).
We prove the intermediate claim HbD: (d1,d2) = (b 0,b 1).
rewrite the current goal using HbEq (from right to left) at position 1.
An exact proof term for the current goal is HbEta.
We prove the intermediate claim Hbcoords: d1 = b 0 ∧ d2 = b 1.
An exact proof term for the current goal is (tuple_eq_coords d1 d2 (b 0) (b 1) HbD).
We prove the intermediate claim Hd1eq: d1 = b 0.
An exact proof term for the current goal is (andEL (d1 = b 0) (d2 = b 1) Hbcoords).
Apply (Hdisj (Rlt (eps_ 1) (b 0))) to the current goal.
Assume Hlt: Rlt c1 d1.
rewrite the current goal using Hc1eq (from right to left) at position 1.
rewrite the current goal using Hd1eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
Assume Hc: c1 = d1 ∧ Rlt c2 d2.
Apply FalseE to the current goal.
We prove the intermediate claim H1lt: Rlt 1 (b 1).
We prove the intermediate claim Heqcd: c1 = d1.
An exact proof term for the current goal is (andEL (c1 = d1) (Rlt c2 d2) Hc).
We prove the intermediate claim Hlt2: Rlt c2 d2.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Hc).
We prove the intermediate claim Hc2eq: c2 = 1.
Use symmetry.
An exact proof term for the current goal is (andER ((eps_ 1) = c1) (1 = c2) Hp0coords).
We prove the intermediate claim Hd2eq: d2 = b 1.
An exact proof term for the current goal is (andER (d1 = b 0) (d2 = b 1) Hbcoords).
We prove the intermediate claim H1lt_d2: Rlt 1 d2.
rewrite the current goal using Hc2eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt2.
rewrite the current goal using Hd2eq (from right to left) at position 1.
An exact proof term for the current goal is H1lt_d2.
An exact proof term for the current goal is (Hb1prop H1lt).
Apply (rational_dense_between_reals (eps_ 1) (b 0) eps_1_in_R Hb0R Hepsltb0) to the current goal.
Let q be given.
Assume Hq_prop.
Apply Hq_prop to the current goal.
Assume HqQ HqIneq.
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
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 (b 0)) HqIneq).
We prove the intermediate claim Hqltb0: Rlt q (b 0).
An exact proof term for the current goal is (andER (Rlt (eps_ 1) q) (Rlt q (b 0)) HqIneq).
We prove the intermediate claim HqU: q ∈ unit_interval.
Apply (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) q HqR) to the current goal.
Apply andI to the current goal.
We will prove ¬ (Rlt q 0).
Assume Hq0: Rlt q 0.
We prove the intermediate claim H0q: Rlt 0 q.
An exact proof term for the current goal is (Rlt_tra 0 (eps_ 1) q eps_1_pos_R Hepsltq).
An exact proof term for the current goal is ((not_Rlt_sym 0 q H0q) Hq0).
We will prove ¬ (Rlt 1 q).
Assume H1q: Rlt 1 q.
We prove the intermediate claim H1b0: Rlt 1 (b 0).
An exact proof term for the current goal is (Rlt_tra 1 q (b 0) H1q Hqltb0).
An exact proof term for the current goal is (Hb0prop H1b0).
Set z to be the term (q,0).
We prove the intermediate claim HzSq: z ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval q 0 HqU zero_in_unit_interval).
We prove the intermediate claim HaEta: a = (a 0,a 1).
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval a HaSq).
We prove the intermediate claim Ha0U: (a 0) ∈ unit_interval.
An exact proof term for the current goal is (ap0_Sigma unit_interval (λ_ : set ⇒ unit_interval) a HaSq).
We prove the intermediate claim Ha0R: (a 0) ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (a 0) Ha0U).
We prove the intermediate claim Hord1: order_rel (setprod R R) a p0.
An exact proof term for the current goal is (andEL (order_rel (setprod R R) a p0) (order_rel (setprod R R) p0 b) Hp0ord).
We prove the intermediate claim Hex_ap: ∃c1 c2 d1 d2 : set, a = (c1,c2) ∧ p0 = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).
An exact proof term for the current goal is (order_rel_setprod_R_R_unfold a p0 Hord1).
We prove the intermediate claim Ha0ltq: Rlt (a 0) q.
Apply Hex_ap to the current goal.
Let c1 be given.
Assume Hc2.
Apply Hc2 to the current goal.
Let c2 be given.
Assume Hd1.
Apply Hd1 to the current goal.
Let d1 be given.
Assume Hd2.
Apply Hd2 to the current goal.
Let d2 be given.
Assume Hcore.
We prove the intermediate claim Hap: a = (c1,c2) ∧ p0 = (d1,d2).
An exact proof term for the current goal is (andEL (a = (c1,c2) ∧ p0 = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim HaEq: a = (c1,c2).
An exact proof term for the current goal is (andEL (a = (c1,c2)) (p0 = (d1,d2)) Hap).
We prove the intermediate claim Hp0Eq: p0 = (d1,d2).
An exact proof term for the current goal is (andER (a = (c1,c2)) (p0 = (d1,d2)) Hap).
We prove the intermediate claim Hdisj: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).
An exact proof term for the current goal is (andER (a = (c1,c2) ∧ p0 = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim HaC: (c1,c2) = (a 0,a 1).
rewrite the current goal using HaEq (from right to left) at position 1.
An exact proof term for the current goal is HaEta.
We prove the intermediate claim HaCcoords: c1 = a 0 ∧ c2 = a 1.
An exact proof term for the current goal is (tuple_eq_coords c1 c2 (a 0) (a 1) HaC).
We prove the intermediate claim Hc1eq: c1 = a 0.
An exact proof term for the current goal is (andEL (c1 = a 0) (c2 = a 1) HaCcoords).
We prove the intermediate claim Hp0def: p0 = (eps_ 1,1).
Use reflexivity.
We prove the intermediate claim Hp0D: (eps_ 1,1) = (d1,d2).
rewrite the current goal using Hp0def (from left to right) at position 1.
An exact proof term for the current goal is Hp0Eq.
We prove the intermediate claim Hp0Dcoords: (eps_ 1) = d1 ∧ 1 = d2.
An exact proof term for the current goal is (tuple_eq_coords (eps_ 1) 1 d1 d2 Hp0D).
We prove the intermediate claim Hd1eq: d1 = eps_ 1.
Use symmetry.
An exact proof term for the current goal is (andEL ((eps_ 1) = d1) (1 = d2) Hp0Dcoords).
Apply (Hdisj (Rlt (a 0) q)) to the current goal.
Assume Hlt: Rlt c1 d1.
We prove the intermediate claim Hlt1: Rlt (a 0) (eps_ 1).
rewrite the current goal using Hc1eq (from right to left) at position 1.
rewrite the current goal using Hd1eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is (Rlt_tra (a 0) (eps_ 1) q Hlt1 Hepsltq).
Assume Hc: c1 = d1 ∧ Rlt c2 d2.
We prove the intermediate claim Heq: c1 = d1.
An exact proof term for the current goal is (andEL (c1 = d1) (Rlt c2 d2) Hc).
We prove the intermediate claim Ha0eq: (a 0) = (eps_ 1).
We will prove (a 0) = (eps_ 1).
rewrite the current goal using Hc1eq (from right to left) at position 1.
rewrite the current goal using Hd1eq (from right to left) at position 1.
An exact proof term for the current goal is Heq.
rewrite the current goal using Ha0eq (from left to right) at position 1.
An exact proof term for the current goal is Hepsltq.
We prove the intermediate claim HzInI: z ∈ I.
rewrite the current goal using HeqI (from left to right).
Apply (SepI ordered_square (λx : set ⇒ order_rel (setprod R R) a x ∧ order_rel (setprod R R) x b) z HzSq) to the current goal.
Apply andI to the current goal.
We will prove order_rel (setprod R R) a z.
rewrite the current goal using HaEta (from left to right).
Apply (order_rel_setprod_R_R_intro (a 0) (a 1) q 0) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Ha0ltq.
We will prove order_rel (setprod R R) z b.
rewrite the current goal using HbEta (from left to right).
Apply (order_rel_setprod_R_R_intro q 0 (b 0) (b 1)) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hqltb0.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (HIU z HzInI).
We prove the intermediate claim HzNotU: ¬ (z ∈ U).
Assume HzU'.
We prove the intermediate claim Hexy: ∃y : set, z = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y).
An exact proof term for the current goal is (SepE2 ordered_square (λp : set ⇒ ∃y : set, p = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)) z HzU').
Apply Hexy to the current goal.
Let y be given.
Assume Hyprop.
We prove the intermediate claim Hpair: z = (eps_ 1,y) ∧ Rlt (eps_ 1) y.
An exact proof term for the current goal is (andEL (z = (eps_ 1,y) ∧ Rlt (eps_ 1) y) (¬ (Rlt 1 y)) Hyprop).
We prove the intermediate claim HzEq: z = (eps_ 1,y).
An exact proof term for the current goal is (andEL (z = (eps_ 1,y)) (Rlt (eps_ 1) y) Hpair).
We prove the intermediate claim Hcoords: q = eps_ 1 ∧ 0 = y.
An exact proof term for the current goal is (tuple_eq_coords q 0 (eps_ 1) y HzEq).
We prove the intermediate claim Hqeq: q = eps_ 1.
An exact proof term for the current goal is (andEL (q = eps_ 1) (0 = y) Hcoords).
We prove the intermediate claim Hbad: Rlt (eps_ 1) (eps_ 1).
rewrite the current goal using Hqeq (from right to left) at position 2.
An exact proof term for the current goal is Hepsltq.
An exact proof term for the current goal is ((not_Rlt_refl (eps_ 1) eps_1_in_R) Hbad).
An exact proof term for the current goal is (HzNotU HzU).
Assume HIlow: I ∈ Blow.
We prove the intermediate claim HIlow_ex: ∃b ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) x b}.
An exact proof term for the current goal is (SepE2 (𝒫 ordered_square) (λJ0 : set ⇒ ∃b0 ∈ ordered_square, J0 = {x ∈ ordered_square|order_rel (setprod R R) x b0}) I HIlow).
Apply HIlow_ex to the current goal.
Let b be given.
Assume Hbprop.
Apply Hbprop to the current goal.
Assume HbSq HeqI.
We prove the intermediate claim Hp0I': p0 ∈ {x ∈ ordered_square|order_rel (setprod R R) x b}.
rewrite the current goal using HeqI (from right to left).
An exact proof term for the current goal is Hp0I.
We prove the intermediate claim Hord2: order_rel (setprod R R) p0 b.
An exact proof term for the current goal is (SepE2 ordered_square (λx : set ⇒ order_rel (setprod R R) x b) p0 Hp0I').
We prove the intermediate claim HbEta: b = (b 0,b 1).
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval b HbSq).
We prove the intermediate claim Hb0U: (b 0) ∈ unit_interval.
An exact proof term for the current goal is (ap0_Sigma unit_interval (λ_ : set ⇒ unit_interval) b HbSq).
We prove the intermediate claim Hb1U: (b 1) ∈ unit_interval.
An exact proof term for the current goal is (ap1_Sigma unit_interval (λ_ : set ⇒ unit_interval) b HbSq).
We prove the intermediate claim Hb0R: (b 0) ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (b 0) Hb0U).
We prove the intermediate claim Hb0prop: ¬ (Rlt 1 (b 0)).
An exact proof term for the current goal is (andER (¬ (Rlt (b 0) 0)) (¬ (Rlt 1 (b 0))) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (b 0) Hb0U)).
We prove the intermediate claim Hb1prop: ¬ (Rlt 1 (b 1)).
An exact proof term for the current goal is (andER (¬ (Rlt (b 1) 0)) (¬ (Rlt 1 (b 1))) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (b 1) Hb1U)).
We prove the intermediate claim Hepsltb0: Rlt (eps_ 1) (b 0).
We prove the intermediate claim Hex_pb: ∃c1 c2 d1 d2 : set, p0 = (c1,c2) ∧ b = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).
An exact proof term for the current goal is (order_rel_setprod_R_R_unfold p0 b Hord2).
Apply Hex_pb to the current goal.
Let c1 be given.
Assume Hc2.
Apply Hc2 to the current goal.
Let c2 be given.
Assume Hd1.
Apply Hd1 to the current goal.
Let d1 be given.
Assume Hd2.
Apply Hd2 to the current goal.
Let d2 be given.
Assume Hcore.
We prove the intermediate claim Hpb: p0 = (c1,c2) ∧ b = (d1,d2).
An exact proof term for the current goal is (andEL (p0 = (c1,c2) ∧ b = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim Hp0Eq: p0 = (c1,c2).
An exact proof term for the current goal is (andEL (p0 = (c1,c2)) (b = (d1,d2)) Hpb).
We prove the intermediate claim HbEq: b = (d1,d2).
An exact proof term for the current goal is (andER (p0 = (c1,c2)) (b = (d1,d2)) Hpb).
We prove the intermediate claim Hdisj: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).
An exact proof term for the current goal is (andER (p0 = (c1,c2) ∧ b = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim Hp0def: p0 = (eps_ 1,1).
Use reflexivity.
We prove the intermediate claim Hp0c: (eps_ 1,1) = (c1,c2).
rewrite the current goal using Hp0def (from left to right) at position 1.
An exact proof term for the current goal is Hp0Eq.
We prove the intermediate claim Hp0coords: (eps_ 1) = c1 ∧ 1 = c2.
An exact proof term for the current goal is (tuple_eq_coords (eps_ 1) 1 c1 c2 Hp0c).
We prove the intermediate claim Hc1eq: c1 = eps_ 1.
Use symmetry.
An exact proof term for the current goal is (andEL ((eps_ 1) = c1) (1 = c2) Hp0coords).
We prove the intermediate claim HbD: (d1,d2) = (b 0,b 1).
rewrite the current goal using HbEq (from right to left) at position 1.
An exact proof term for the current goal is HbEta.
We prove the intermediate claim Hbcoords: d1 = b 0 ∧ d2 = b 1.
An exact proof term for the current goal is (tuple_eq_coords d1 d2 (b 0) (b 1) HbD).
We prove the intermediate claim Hd1eq: d1 = b 0.
An exact proof term for the current goal is (andEL (d1 = b 0) (d2 = b 1) Hbcoords).
Apply (Hdisj (Rlt (eps_ 1) (b 0))) to the current goal.
Assume Hlt: Rlt c1 d1.
rewrite the current goal using Hc1eq (from right to left) at position 1.
rewrite the current goal using Hd1eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
Assume Hc: c1 = d1 ∧ Rlt c2 d2.
Apply FalseE to the current goal.
We prove the intermediate claim H1lt: Rlt 1 (b 1).
We prove the intermediate claim Hlt2: Rlt c2 d2.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Hc).
We prove the intermediate claim Hc2eq: c2 = 1.
Use symmetry.
An exact proof term for the current goal is (andER ((eps_ 1) = c1) (1 = c2) Hp0coords).
We prove the intermediate claim Hd2eq: d2 = b 1.
An exact proof term for the current goal is (andER (d1 = b 0) (d2 = b 1) Hbcoords).
We prove the intermediate claim H1lt_d2: Rlt 1 d2.
rewrite the current goal using Hc2eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt2.
rewrite the current goal using Hd2eq (from right to left) at position 1.
An exact proof term for the current goal is H1lt_d2.
An exact proof term for the current goal is (Hb1prop H1lt).
Apply (rational_dense_between_reals (eps_ 1) (b 0) eps_1_in_R Hb0R Hepsltb0) to the current goal.
Let q be given.
Assume Hq_prop.
Apply Hq_prop to the current goal.
Assume HqQ HqIneq.
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
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 (b 0)) HqIneq).
We prove the intermediate claim Hqltb0: Rlt q (b 0).
An exact proof term for the current goal is (andER (Rlt (eps_ 1) q) (Rlt q (b 0)) HqIneq).
We prove the intermediate claim HqU: q ∈ unit_interval.
Apply (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) q HqR) to the current goal.
Apply andI to the current goal.
We will prove ¬ (Rlt q 0).
Assume Hq0: Rlt q 0.
We prove the intermediate claim H0q: Rlt 0 q.
An exact proof term for the current goal is (Rlt_tra 0 (eps_ 1) q eps_1_pos_R Hepsltq).
An exact proof term for the current goal is ((not_Rlt_sym 0 q H0q) Hq0).
We will prove ¬ (Rlt 1 q).
Assume H1q: Rlt 1 q.
We prove the intermediate claim H1b0: Rlt 1 (b 0).
An exact proof term for the current goal is (Rlt_tra 1 q (b 0) H1q Hqltb0).
An exact proof term for the current goal is (Hb0prop H1b0).
Set z to be the term (q,0).
We prove the intermediate claim HzSq: z ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval q 0 HqU zero_in_unit_interval).
We prove the intermediate claim HzInI: z ∈ I.
rewrite the current goal using HeqI (from left to right).
Apply (SepI ordered_square (λx : set ⇒ order_rel (setprod R R) x b) z HzSq) to the current goal.
rewrite the current goal using HbEta (from left to right).
Apply (order_rel_setprod_R_R_intro q 0 (b 0) (b 1)) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hqltb0.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (HIU z HzInI).
We prove the intermediate claim HzNotU: ¬ (z ∈ U).
Assume HzU'.
We prove the intermediate claim Hexy: ∃y : set, z = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y).
An exact proof term for the current goal is (SepE2 ordered_square (λp : set ⇒ ∃y : set, p = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)) z HzU').
Apply Hexy to the current goal.
Let y be given.
Assume Hyprop.
We prove the intermediate claim Hpair: z = (eps_ 1,y) ∧ Rlt (eps_ 1) y.
An exact proof term for the current goal is (andEL (z = (eps_ 1,y) ∧ Rlt (eps_ 1) y) (¬ (Rlt 1 y)) Hyprop).
We prove the intermediate claim HzEq: z = (eps_ 1,y).
An exact proof term for the current goal is (andEL (z = (eps_ 1,y)) (Rlt (eps_ 1) y) Hpair).
We prove the intermediate claim Hcoords: q = eps_ 1 ∧ 0 = y.
An exact proof term for the current goal is (tuple_eq_coords q 0 (eps_ 1) y HzEq).
We prove the intermediate claim Hqeq: q = eps_ 1.
An exact proof term for the current goal is (andEL (q = eps_ 1) (0 = y) Hcoords).
We prove the intermediate claim Hbad: Rlt (eps_ 1) (eps_ 1).
rewrite the current goal using Hqeq (from right to left) at position 2.
An exact proof term for the current goal is Hepsltq.
An exact proof term for the current goal is ((not_Rlt_refl (eps_ 1) eps_1_in_R) Hbad).
An exact proof term for the current goal is (HzNotU HzU).
Assume HIup: I ∈ Bup.
We prove the intermediate claim HIup_ex: ∃a ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) a x}.
An exact proof term for the current goal is (SepE2 (𝒫 ordered_square) (λJ0 : set ⇒ ∃a0 ∈ ordered_square, J0 = {x ∈ ordered_square|order_rel (setprod R R) a0 x}) I HIup).
Apply HIup_ex to the current goal.
Let a be given.
Assume Haprop.
Apply Haprop to the current goal.
Assume HaSq HeqI.
We prove the intermediate claim Hp0I': p0 ∈ {x ∈ ordered_square|order_rel (setprod R R) a x}.
rewrite the current goal using HeqI (from right to left).
An exact proof term for the current goal is Hp0I.
We prove the intermediate claim Hord1: order_rel (setprod R R) a p0.
An exact proof term for the current goal is (SepE2 ordered_square (λx : set ⇒ order_rel (setprod R R) a x) p0 Hp0I').
We prove the intermediate claim HaEta: a = (a 0,a 1).
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval a HaSq).
We prove the intermediate claim Ha0U: (a 0) ∈ unit_interval.
An exact proof term for the current goal is (ap0_Sigma unit_interval (λ_ : set ⇒ unit_interval) a HaSq).
We prove the intermediate claim Ha0R: (a 0) ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (a 0) Ha0U).
We prove the intermediate claim Ha0lt1: Rlt (a 0) 1.
We prove the intermediate claim Hex_ap: ∃c1 c2 d1 d2 : set, a = (c1,c2) ∧ p0 = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).
An exact proof term for the current goal is (order_rel_setprod_R_R_unfold a p0 Hord1).
Apply Hex_ap to the current goal.
Let c1 be given.
Assume Hc2.
Apply Hc2 to the current goal.
Let c2 be given.
Assume Hd1.
Apply Hd1 to the current goal.
Let d1 be given.
Assume Hd2.
Apply Hd2 to the current goal.
Let d2 be given.
Assume Hcore.
We prove the intermediate claim Hap: a = (c1,c2) ∧ p0 = (d1,d2).
An exact proof term for the current goal is (andEL (a = (c1,c2) ∧ p0 = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim HaEq: a = (c1,c2).
An exact proof term for the current goal is (andEL (a = (c1,c2)) (p0 = (d1,d2)) Hap).
We prove the intermediate claim Hp0Eq: p0 = (d1,d2).
An exact proof term for the current goal is (andER (a = (c1,c2)) (p0 = (d1,d2)) Hap).
We prove the intermediate claim Hdisj: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).
An exact proof term for the current goal is (andER (a = (c1,c2) ∧ p0 = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim HaC: (c1,c2) = (a 0,a 1).
rewrite the current goal using HaEq (from right to left) at position 1.
An exact proof term for the current goal is HaEta.
We prove the intermediate claim HaCcoords: c1 = a 0 ∧ c2 = a 1.
An exact proof term for the current goal is (tuple_eq_coords c1 c2 (a 0) (a 1) HaC).
We prove the intermediate claim Hc1eq: c1 = a 0.
An exact proof term for the current goal is (andEL (c1 = a 0) (c2 = a 1) HaCcoords).
We prove the intermediate claim Hp0def: p0 = (eps_ 1,1).
Use reflexivity.
We prove the intermediate claim Hp0D: (eps_ 1,1) = (d1,d2).
rewrite the current goal using Hp0def (from left to right) at position 1.
An exact proof term for the current goal is Hp0Eq.
We prove the intermediate claim Hp0Dcoords: (eps_ 1) = d1 ∧ 1 = d2.
An exact proof term for the current goal is (tuple_eq_coords (eps_ 1) 1 d1 d2 Hp0D).
We prove the intermediate claim Hd1eq: d1 = eps_ 1.
Use symmetry.
An exact proof term for the current goal is (andEL ((eps_ 1) = d1) (1 = d2) Hp0Dcoords).
Apply (Hdisj (Rlt (a 0) 1)) to the current goal.
Assume Hlt: Rlt c1 d1.
We prove the intermediate claim Ha0lteps: Rlt (a 0) (eps_ 1).
rewrite the current goal using Hc1eq (from right to left) at position 1.
rewrite the current goal using Hd1eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is (Rlt_tra (a 0) (eps_ 1) 1 Ha0lteps eps_1_lt1_R).
Assume Hc: c1 = d1 ∧ Rlt c2 d2.
We prove the intermediate claim Heq: c1 = d1.
An exact proof term for the current goal is (andEL (c1 = d1) (Rlt c2 d2) Hc).
We prove the intermediate claim Ha0eq: (a 0) = (eps_ 1).
We will prove (a 0) = (eps_ 1).
rewrite the current goal using Hc1eq (from right to left) at position 1.
rewrite the current goal using Hd1eq (from right to left) at position 1.
An exact proof term for the current goal is Heq.
rewrite the current goal using Ha0eq (from left to right) at position 1.
An exact proof term for the current goal is eps_1_lt1_R.
Set z to be the term (1,0).
We prove the intermediate claim HzSq: z ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval 1 0 one_in_unit_interval zero_in_unit_interval).
We prove the intermediate claim HzInI: z ∈ I.
rewrite the current goal using HeqI (from left to right).
Apply (SepI ordered_square (λx : set ⇒ order_rel (setprod R R) a x) z HzSq) to the current goal.
rewrite the current goal using HaEta (from left to right).
Apply (order_rel_setprod_R_R_intro (a 0) (a 1) 1 0) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Ha0lt1.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (HIU z HzInI).
We prove the intermediate claim HzNotU: ¬ (z ∈ U).
Assume HzU'.
We prove the intermediate claim Hexy: ∃y : set, z = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y).
An exact proof term for the current goal is (SepE2 ordered_square (λp : set ⇒ ∃y : set, p = (eps_ 1,y) ∧ Rlt (eps_ 1) y ∧ ¬ (Rlt 1 y)) z HzU').
Apply Hexy to the current goal.
Let y be given.
Assume Hyprop.
We prove the intermediate claim Hpair: z = (eps_ 1,y) ∧ Rlt (eps_ 1) y.
An exact proof term for the current goal is (andEL (z = (eps_ 1,y) ∧ Rlt (eps_ 1) y) (¬ (Rlt 1 y)) Hyprop).
We prove the intermediate claim HzEq: z = (eps_ 1,y).
An exact proof term for the current goal is (andEL (z = (eps_ 1,y)) (Rlt (eps_ 1) y) Hpair).
We prove the intermediate claim Hcoords: 1 = eps_ 1 ∧ 0 = y.
An exact proof term for the current goal is (tuple_eq_coords 1 0 (eps_ 1) y HzEq).
We prove the intermediate claim H1eq: 1 = eps_ 1.
An exact proof term for the current goal is (andEL (1 = eps_ 1) (0 = y) Hcoords).
We prove the intermediate claim Hbad: Rlt (eps_ 1) (eps_ 1).
rewrite the current goal using H1eq (from right to left) at position 2.
An exact proof term for the current goal is eps_1_lt1_R.
An exact proof term for the current goal is ((not_Rlt_refl (eps_ 1) eps_1_in_R) Hbad).
An exact proof term for the current goal is (HzNotU HzU).
An exact proof term for the current goal is (HUnord HUord).
∎