We will prove closure_of ordered_square ordered_square_topology ordsq_E = ordsq_E_closure.
Apply set_ext to the current goal.
Let p be given.
Assume Hpcl: p ∈ closure_of ordered_square ordered_square_topology ordsq_E.
We will prove p ∈ ordsq_E_closure.
We prove the intermediate claim HpSq: p ∈ ordered_square.
An exact proof term for the current goal is (SepE1 ordered_square (λx0 : set ⇒ ∀U : set, U ∈ ordered_square_topology → x0 ∈ U → U ∩ ordsq_E ≠ Empty) p Hpcl).
We prove the intermediate claim Hcond: ∀U : set, U ∈ ordered_square_topology → p ∈ U → U ∩ ordsq_E ≠ Empty.
An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ ∀U : set, U ∈ ordered_square_topology → x0 ∈ U → U ∩ ordsq_E ≠ Empty) p Hpcl).
Set a to be the term p 0.
Set y to be the term p 1.
We prove the intermediate claim HaU: a ∈ unit_interval.
An exact proof term for the current goal is (ap0_Sigma unit_interval (λ_ : set ⇒ unit_interval) p HpSq).
We prove the intermediate claim HyU: y ∈ 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 HaR: a ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) a HaU).
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) y HyU).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HepsS: SNo (eps_ 1).
An exact proof term for the current goal is SNo_eps_1.
We prove the intermediate claim HpEta: p = (a,y).
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval p HpSq).
Apply (SNoLt_trichotomy_or_impred a (eps_ 1) HaS HepsS (p ∈ ordsq_E_closure)) to the current goal.
Assume Halt: a < (eps_ 1).
We will prove p ∈ ordsq_E_closure.
Apply FalseE to the current goal.
Set b0 to be the term (eps_ 1,0).
Set U0 to be the term {x ∈ ordered_square|order_rel (setprod R R) x b0}.
We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 ordered_square.
An exact proof term for the current goal is (Sep_In_Power ordered_square (λx0 : set ⇒ order_rel (setprod R R) x0 b0)).
We prove the intermediate claim Hb0Sq: b0 ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval (eps_ 1) 0 eps_1_in_unit_interval zero_in_unit_interval).
We prove the intermediate claim HU0basis: U0 ∈ ordered_square_order_basis.
Set Bint to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) a0 x ∧ order_rel (setprod R R) x b}}.
Set Blow to be the term {I ∈ 𝒫 ordered_square|∃b ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) x b}}.
Set Bup to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) a0 x}}.
We prove the intermediate claim Hdef: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply binunionI1 to the current goal.
Apply binunionI2 to the current goal.
We will prove U0 ∈ Blow.
Apply (SepI (𝒫 ordered_square) (λI : set ⇒ ∃b ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) x b}) U0) to the current goal.
An exact proof term for the current goal is HU0Pow.
We use b0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb0Sq.
Use reflexivity.
We prove the intermediate claim HU0top: U0 ∈ ordered_square_topology.
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 left to right).
An exact proof term for the current goal is (generated_topology_contains_elem ordered_square ordered_square_order_basis U0 HU0Pow HU0basis).
We prove the intermediate claim Hrlt: Rlt a (eps_ 1).
An exact proof term for the current goal is (RltI a (eps_ 1) HaR eps_1_in_R Halt).
We prove the intermediate claim Hordpb: order_rel (setprod R R) p b0.
rewrite the current goal using HpEta (from left to right).
Apply (order_rel_setprod_R_R_intro a y (eps_ 1) 0) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hrlt.
We prove the intermediate claim HpU0: p ∈ U0.
Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) x0 b0) p HpSq) to the current goal.
An exact proof term for the current goal is Hordpb.
We prove the intermediate claim HcapSub: U0 ∩ ordsq_E ⊆ Empty.
Let z be given.
Assume Hz: z ∈ U0 ∩ ordsq_E.
We will prove z ∈ Empty.
We prove the intermediate claim HzU: z ∈ U0.
An exact proof term for the current goal is (binintersectE1 U0 ordsq_E z Hz).
We prove the intermediate claim HzE: z ∈ ordsq_E.
An exact proof term for the current goal is (binintersectE2 U0 ordsq_E z Hz).
We prove the intermediate claim HzOrd: order_rel (setprod R R) z b0.
An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) x0 b0) z HzU).
We prove the intermediate claim HzEx: ∃y0 : set, z = (eps_ 1,y0) ∧ Rlt 0 y0 ∧ Rlt y0 1.
An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃y0 : set, p0 = (eps_ 1,y0) ∧ Rlt 0 y0 ∧ Rlt y0 1) z HzE).
Apply HzEx to the current goal.
Let y0 be given.
Assume Hy0pack.
Apply Hy0pack to the current goal.
Assume Hcore Hy0lt1.
Apply Hcore to the current goal.
Assume Hzpair Hy0pos.
We prove the intermediate claim Hny0lt0: ¬ (Rlt y0 0).
An exact proof term for the current goal is (not_Rlt_sym 0 y0 Hy0pos).
We prove the intermediate claim HzOrd2: order_rel (setprod R R) (eps_ 1,y0) b0.
rewrite the current goal using Hzpair (from right to left) at position 1.
An exact proof term for the current goal is HzOrd.
We prove the intermediate claim Hcase: ∃c1 c2 d1 d2 : set, (eps_ 1,y0) = (c1,c2) ∧ b0 = (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 (eps_ 1,y0) b0 HzOrd2).
Apply Hcase 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.
Apply Hcore to the current goal.
Assume Hab Hdisj.
Apply Hab to the current goal.
Assume HcEq HdEq.
We prove the intermediate claim HcPair: (c1,c2) = (eps_ 1,y0).
rewrite the current goal using HcEq (from right to left) at position 1.
Use reflexivity.
We prove the intermediate claim Hc1eq: c1 = (eps_ 1).
We will prove c1 = (eps_ 1).
rewrite the current goal using (tuple_2_0_eq c1 c2) (from right to left) at position 1.
rewrite the current goal using HcPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) y0).
We prove the intermediate claim Hc2eq: c2 = y0.
We will prove c2 = y0.
rewrite the current goal using (tuple_2_1_eq c1 c2) (from right to left) at position 1.
rewrite the current goal using HcPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq (eps_ 1) y0).
We prove the intermediate claim Hb0eq: b0 = (eps_ 1,0).
Use reflexivity.
We prove the intermediate claim HdPair: (d1,d2) = (eps_ 1,0).
rewrite the current goal using Hb0eq (from right to left) at position 1.
rewrite the current goal using HdEq (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hd1eq: d1 = (eps_ 1).
We will prove d1 = (eps_ 1).
rewrite the current goal using (tuple_2_0_eq d1 d2) (from right to left) at position 1.
rewrite the current goal using HdPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) 0).
We prove the intermediate claim Hd2eq: d2 = 0.
We will prove d2 = 0.
rewrite the current goal using (tuple_2_1_eq d1 d2) (from right to left) at position 1.
rewrite the current goal using HdPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq (eps_ 1) 0).
Apply Hdisj to the current goal.
Assume Hlt: Rlt c1 d1.
Apply FalseE to the current goal.
We prove the intermediate claim Hbad: Rlt (eps_ 1) (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 ((not_Rlt_refl (eps_ 1) eps_1_in_R) Hbad).
Assume Heq: c1 = d1 ∧ Rlt c2 d2.
Apply FalseE to the current goal.
We prove the intermediate claim Hy0lt0: Rlt y0 0.
rewrite the current goal using Hc2eq (from right to left) at position 1.
rewrite the current goal using Hd2eq (from right to left) at position 1.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Heq).
An exact proof term for the current goal is (Hny0lt0 Hy0lt0).
We prove the intermediate claim HcapEq: U0 ∩ ordsq_E = Empty.
An exact proof term for the current goal is (Empty_Subq_eq (U0 ∩ ordsq_E) HcapSub).
An exact proof term for the current goal is ((Hcond U0 HU0top HpU0) HcapEq).
Assume Haeq: a = (eps_ 1).
We will prove p ∈ ordsq_E_closure.
We prove the intermediate claim HdefEcl: ordsq_E_closure = (ordsq_E ∪ {(eps_ 1,0)}) ∪ {(eps_ 1,1)}.
Use reflexivity.
rewrite the current goal using HdefEcl (from left to right).
Apply (xm (y = 0)) to the current goal.
Assume Hy0: y = 0.
Apply binunionI1 to the current goal.
Apply binunionI2 to the current goal.
We prove the intermediate claim HpEq: p = (eps_ 1,0).
rewrite the current goal using HpEta (from left to right).
rewrite the current goal using Haeq (from left to right).
rewrite the current goal using Hy0 (from left to right).
Use reflexivity.
rewrite the current goal using HpEq (from left to right).
An exact proof term for the current goal is (SingI (eps_ 1,0)).
Assume Hyn0: ¬ (y = 0).
Apply (xm (y = 1)) to the current goal.
Assume Hy1: y = 1.
Apply binunionI2 to the current goal.
We prove the intermediate claim HpEq: p = (eps_ 1,1).
rewrite the current goal using HpEta (from left to right).
rewrite the current goal using Haeq (from left to right).
rewrite the current goal using Hy1 (from left to right).
Use reflexivity.
rewrite the current goal using HpEq (from left to right).
An exact proof term for the current goal is (SingI (eps_ 1,1)).
Assume Hyn1: ¬ (y = 1).
Apply binunionI1 to the current goal.
Apply binunionI1 to the current goal.
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 Hnylt0: ¬ (Rlt y 0).
An exact proof term for the current goal is (andEL (¬ (Rlt y 0)) (¬ (Rlt 1 y)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) y HyU)).
We prove the intermediate claim Hn1lty: ¬ (Rlt 1 y).
An exact proof term for the current goal is (andER (¬ (Rlt y 0)) (¬ (Rlt 1 y)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) y HyU)).
We prove the intermediate claim Hypos: Rlt 0 y.
Apply (SNoLt_trichotomy_or_impred y 0 HyS SNo_0 (Rlt 0 y)) to the current goal.
Assume Hylt0: y < 0.
Apply FalseE to the current goal.
We prove the intermediate claim Htmp: Rlt y 0.
An exact proof term for the current goal is (RltI y 0 HyR real_0 Hylt0).
An exact proof term for the current goal is (Hnylt0 Htmp).
Assume Hyeq0: y = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hyn0 Hyeq0).
Assume H0lty: 0 < y.
An exact proof term for the current goal is (RltI 0 y real_0 HyR H0lty).
We prove the intermediate claim Hylt1: Rlt y 1.
Apply (SNoLt_trichotomy_or_impred 1 y SNo_1 HyS (Rlt y 1)) to the current goal.
Assume H1lty: 1 < y.
Apply FalseE to the current goal.
We prove the intermediate claim Htmp: Rlt 1 y.
An exact proof term for the current goal is (RltI 1 y real_1 HyR H1lty).
An exact proof term for the current goal is (Hn1lty Htmp).
Assume H1eqy: 1 = y.
Apply FalseE to the current goal.
We prove the intermediate claim Hyeq1: y = 1.
rewrite the current goal using H1eqy (from right to left) at position 1.
Use reflexivity.
An exact proof term for the current goal is (Hyn1 Hyeq1).
Assume Hylt1': y < 1.
An exact proof term for the current goal is (RltI y 1 HyR real_1 Hylt1').
Apply (SepI ordered_square (λp0 : set ⇒ ∃y0 : set, p0 = (eps_ 1,y0) ∧ Rlt 0 y0 ∧ Rlt y0 1) p HpSq) to the current goal.
We use y to witness the existential quantifier.
We will prove p = (eps_ 1,y) ∧ Rlt 0 y ∧ Rlt y 1.
Apply andI to the current goal.
We will prove p = (eps_ 1,y) ∧ Rlt 0 y.
Apply andI to the current goal.
rewrite the current goal using HpEta (from left to right) at position 1.
rewrite the current goal using Haeq (from left to right) at position 1.
Use reflexivity.
An exact proof term for the current goal is Hypos.
An exact proof term for the current goal is Hylt1.
Assume Hgt: (eps_ 1) < a.
We will prove p ∈ ordsq_E_closure.
Apply FalseE to the current goal.
Set a0 to be the term (eps_ 1,1).
Set U1 to be the term {x ∈ ordered_square|order_rel (setprod R R) a0 x}.
We prove the intermediate claim HU1Pow: U1 ∈ 𝒫 ordered_square.
An exact proof term for the current goal is (Sep_In_Power ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0)).
We prove the intermediate claim Ha0Sq: a0 ∈ 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 HU1basis: U1 ∈ ordered_square_order_basis.
Set Bint to be the term {I ∈ 𝒫 ordered_square|∃a1 ∈ ordered_square, ∃b ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) a1 x ∧ order_rel (setprod R R) x b}}.
Set Blow to be the term {I ∈ 𝒫 ordered_square|∃b ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) x b}}.
Set Bup to be the term {I ∈ 𝒫 ordered_square|∃a1 ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) a1 x}}.
We prove the intermediate claim Hdef: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply binunionI2 to the current goal.
We will prove U1 ∈ Bup.
Apply (SepI (𝒫 ordered_square) (λI : set ⇒ ∃a1 ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) a1 x}) U1) to the current goal.
An exact proof term for the current goal is HU1Pow.
We use a0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0Sq.
Use reflexivity.
We prove the intermediate claim HU1top: U1 ∈ ordered_square_topology.
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 left to right).
An exact proof term for the current goal is (generated_topology_contains_elem ordered_square ordered_square_order_basis U1 HU1Pow HU1basis).
We prove the intermediate claim Hrlt: Rlt (eps_ 1) a.
An exact proof term for the current goal is (RltI (eps_ 1) a eps_1_in_R HaR Hgt).
We prove the intermediate claim Horda0p: order_rel (setprod R R) a0 p.
rewrite the current goal using HpEta (from left to right) at position 1.
Apply (order_rel_setprod_R_R_intro (eps_ 1) 1 a y) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hrlt.
We prove the intermediate claim HpU1: p ∈ U1.
Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0) p HpSq) to the current goal.
An exact proof term for the current goal is Horda0p.
We prove the intermediate claim HcapSub: U1 ∩ ordsq_E ⊆ Empty.
Let z be given.
Assume Hz: z ∈ U1 ∩ ordsq_E.
We will prove z ∈ Empty.
We prove the intermediate claim HzU: z ∈ U1.
An exact proof term for the current goal is (binintersectE1 U1 ordsq_E z Hz).
We prove the intermediate claim HzE: z ∈ ordsq_E.
An exact proof term for the current goal is (binintersectE2 U1 ordsq_E z Hz).
We prove the intermediate claim HzOrd: order_rel (setprod R R) a0 z.
An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0) z HzU).
We prove the intermediate claim HzEx: ∃y0 : set, z = (eps_ 1,y0) ∧ Rlt 0 y0 ∧ Rlt y0 1.
An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃y0 : set, p0 = (eps_ 1,y0) ∧ Rlt 0 y0 ∧ Rlt y0 1) z HzE).
Apply HzEx to the current goal.
Let y0 be given.
Assume Hy0pack.
Apply Hy0pack to the current goal.
Assume Hcore Hy0lt1.
Apply Hcore to the current goal.
Assume Hzpair Hy0pos.
We prove the intermediate claim Hn1lty0: ¬ (Rlt 1 y0).
An exact proof term for the current goal is (not_Rlt_sym y0 1 Hy0lt1).
We prove the intermediate claim HzOrd2: order_rel (setprod R R) a0 (eps_ 1,y0).
rewrite the current goal using Hzpair (from right to left) at position 1.
An exact proof term for the current goal is HzOrd.
We prove the intermediate claim Hcase: ∃c1 c2 d1 d2 : set, a0 = (c1,c2) ∧ (eps_ 1,y0) = (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 a0 (eps_ 1,y0) HzOrd2).
Apply Hcase 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.
Apply Hcore to the current goal.
Assume Hab Hdisj.
Apply Hab to the current goal.
Assume HcEq HdEq.
We prove the intermediate claim Ha0eq: a0 = (eps_ 1,1).
Use reflexivity.
We prove the intermediate claim HcPair: (c1,c2) = (eps_ 1,1).
rewrite the current goal using Ha0eq (from right to left) at position 1.
rewrite the current goal using HcEq (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hc1eq: c1 = (eps_ 1).
We will prove c1 = (eps_ 1).
rewrite the current goal using (tuple_2_0_eq c1 c2) (from right to left) at position 1.
rewrite the current goal using HcPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) 1).
We prove the intermediate claim Hc2eq: c2 = 1.
We will prove c2 = 1.
rewrite the current goal using (tuple_2_1_eq c1 c2) (from right to left) at position 1.
rewrite the current goal using HcPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq (eps_ 1) 1).
We prove the intermediate claim HdPair: (d1,d2) = (eps_ 1,y0).
rewrite the current goal using HdEq (from right to left) at position 1.
Use reflexivity.
We prove the intermediate claim Hd1eq: d1 = (eps_ 1).
We will prove d1 = (eps_ 1).
rewrite the current goal using (tuple_2_0_eq d1 d2) (from right to left) at position 1.
rewrite the current goal using HdPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) y0).
We prove the intermediate claim Hd2eq: d2 = y0.
We will prove d2 = y0.
rewrite the current goal using (tuple_2_1_eq d1 d2) (from right to left) at position 1.
rewrite the current goal using HdPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq (eps_ 1) y0).
Apply Hdisj to the current goal.
Assume Hlt: Rlt c1 d1.
Apply FalseE to the current goal.
We prove the intermediate claim Hbad: Rlt (eps_ 1) (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 ((not_Rlt_refl (eps_ 1) eps_1_in_R) Hbad).
Assume Heq: c1 = d1 ∧ Rlt c2 d2.
Apply FalseE to the current goal.
We prove the intermediate claim H1lty0: Rlt 1 y0.
rewrite the current goal using Hc2eq (from right to left) at position 1.
rewrite the current goal using Hd2eq (from right to left) at position 1.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Heq).
An exact proof term for the current goal is (Hn1lty0 H1lty0).
We prove the intermediate claim HcapEq: U1 ∩ ordsq_E = Empty.
An exact proof term for the current goal is (Empty_Subq_eq (U1 ∩ ordsq_E) HcapSub).
An exact proof term for the current goal is ((Hcond U1 HU1top HpU1) HcapEq).
Let p be given.
Assume Hp: p ∈ ordsq_E_closure.
We will prove p ∈ closure_of ordered_square ordered_square_topology ordsq_E.
Apply (binunionE (ordsq_E ∪ {(eps_ 1,0)}) {(eps_ 1,1)} p Hp) to the current goal.
Assume HpL: p ∈ (ordsq_E ∪ {(eps_ 1,0)}).
Apply (binunionE ordsq_E {(eps_ 1,0)} p HpL) to the current goal.
Assume HpE: p ∈ ordsq_E.
We prove the intermediate claim HpSq: p ∈ ordered_square.
An exact proof term for the current goal is (SepE1 ordered_square (λp0 : set ⇒ ∃y0 : set, p0 = (eps_ 1,y0) ∧ Rlt 0 y0 ∧ Rlt y0 1) p HpE).
We prove the intermediate claim Hdefcl: closure_of ordered_square ordered_square_topology ordsq_E = {x ∈ ordered_square|∀U : set, U ∈ ordered_square_topology → x ∈ U → U ∩ ordsq_E ≠ Empty}.
Use reflexivity.
rewrite the current goal using Hdefcl (from left to right).
Apply (SepI ordered_square (λx0 : set ⇒ ∀U : set, U ∈ ordered_square_topology → x0 ∈ U → U ∩ ordsq_E ≠ Empty) p HpSq) to the current goal.
Let U be given.
Assume HU: U ∈ ordered_square_topology.
Assume HpU: p ∈ U.
We will prove U ∩ ordsq_E ≠ Empty.
Assume Hempty: U ∩ ordsq_E = Empty.
We prove the intermediate claim HpUE: p ∈ U ∩ ordsq_E.
An exact proof term for the current goal is (binintersectI U ordsq_E p HpU HpE).
We prove the intermediate claim HpEmpty: p ∈ Empty.
rewrite the current goal using Hempty (from right to left).
An exact proof term for the current goal is HpUE.
An exact proof term for the current goal is (EmptyE p HpEmpty).
Assume Hp0: p ∈ {(eps_ 1,0)}.
We prove the intermediate claim HpEq: p = (eps_ 1,0).
An exact proof term for the current goal is (SingE (eps_ 1,0) p Hp0).
rewrite the current goal using HpEq (from left to right).
Set p0 to be the term (eps_ 1,0).
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) 0 eps_1_in_unit_interval zero_in_unit_interval).
We prove the intermediate claim Hdefcl: closure_of ordered_square ordered_square_topology ordsq_E = {x ∈ ordered_square|∀U : set, U ∈ ordered_square_topology → x ∈ U → U ∩ ordsq_E ≠ Empty}.
Use reflexivity.
rewrite the current goal using Hdefcl (from left to right).
Apply (SepI ordered_square (λx0 : set ⇒ ∀U : set, U ∈ ordered_square_topology → x0 ∈ U → U ∩ ordsq_E ≠ Empty) p0 Hp0Sq) to the current goal.
Let U be given.
Assume HUtop: U ∈ ordered_square_topology.
Assume Hp0U: p0 ∈ U.
We will prove U ∩ ordsq_E ≠ Empty.
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 HUtop.
We prove the intermediate claim HexI: ∃I ∈ ordered_square_order_basis, p0 ∈ I ∧ I ⊆ U.
An exact proof term for the current goal is (generated_topology_local_refine ordered_square ordered_square_order_basis U p0 HUgt 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|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, J = {x ∈ ordered_square|order_rel (setprod R R) a0 x ∧ order_rel (setprod R R) x b0}}.
Set Blow to be the term {J ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, J = {x ∈ ordered_square|order_rel (setprod R R) x b0}}.
Set Bup to be the term {J ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, J = {x ∈ ordered_square|order_rel (setprod R R) a0 x}}.
We prove the intermediate claim HIcase: I ∈ ((Bint ∪ Blow) ∪ Bup).
We prove the intermediate claim HdefB: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).
Use reflexivity.
rewrite the current goal using HdefB (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: ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) a0 x ∧ order_rel (setprod R R) x b0}.
An exact proof term for the current goal is (SepE2 (𝒫 ordered_square) (λJ0 : set ⇒ ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, J0 = {x ∈ ordered_square|order_rel (setprod R R) a0 x ∧ order_rel (setprod R R) x b0}) I HIint).
Apply HIint_ex to the current goal.
Let a0 be given.
Assume Ha0rest.
Apply Ha0rest to the current goal.
Assume Ha0Sq Hb0core.
Apply Hb0core to the current goal.
Let b0 be given.
Assume Hb0pack.
Apply Hb0pack to the current goal.
Assume Hb0Sq HeqI.
We prove the intermediate claim Hp0I2: p0 ∈ {x ∈ ordered_square|order_rel (setprod R R) a0 x ∧ order_rel (setprod R R) x b0}.
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 Hp0props: order_rel (setprod R R) a0 p0 ∧ order_rel (setprod R R) p0 b0.
An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0) p0 Hp0I2).
Apply Hp0props to the current goal.
Assume Ha0p0 Hp0b0.
We prove the intermediate claim Hcase: ∃c1 c2 d1 d2 : set, p0 = (c1,c2) ∧ b0 = (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 b0 Hp0b0).
Apply Hcase 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.
Apply Hcore to the current goal.
Assume Hab Hdisj.
Apply Hab to the current goal.
Assume Hp0Eq Hb0Eq.
We prove the intermediate claim Hp0def: p0 = (eps_ 1,0).
Use reflexivity.
We prove the intermediate claim HcPair: (c1,c2) = (eps_ 1,0).
rewrite the current goal using Hp0def (from right to left) at position 1.
rewrite the current goal using Hp0Eq (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hc1eq: c1 = (eps_ 1).
We will prove c1 = (eps_ 1).
rewrite the current goal using (tuple_2_0_eq c1 c2) (from right to left) at position 1.
rewrite the current goal using HcPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) 0).
We prove the intermediate claim Hc2eq: c2 = 0.
We will prove c2 = 0.
rewrite the current goal using (tuple_2_1_eq c1 c2) (from right to left) at position 1.
rewrite the current goal using HcPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq (eps_ 1) 0).
We prove the intermediate claim HdPair: (d1,d2) = b0.
rewrite the current goal using Hb0Eq (from right to left) at position 1.
Use reflexivity.
We prove the intermediate claim Hd2eq: d2 = (b0 1).
We will prove d2 = (b0 1).
rewrite the current goal using (tuple_2_1_eq d1 d2) (from right to left) at position 1.
rewrite the current goal using HdPair (from left to right) at position 1.
Use reflexivity.
Apply Hdisj to the current goal.
Assume Hlt: Rlt c1 d1.
Set w to be the term (eps_ 1,eps_ 1).
We prove the intermediate claim HwE: w ∈ ordsq_E.
We prove the intermediate claim Hweq: w = (eps_ 1,eps_ 1).
Use reflexivity.
rewrite the current goal using Hweq (from left to right).
An exact proof term for the current goal is ordsq_eps1_eps1_in_E.
We prove the intermediate claim HwSq: w ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval (eps_ 1) (eps_ 1) eps_1_in_unit_interval eps_1_in_unit_interval).
We prove the intermediate claim Hp0w: order_rel (setprod R R) p0 w.
Apply (order_rel_setprod_R_R_intro (eps_ 1) 0 (eps_ 1) (eps_ 1)) 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 eps_1_pos_R.
We prove the intermediate claim Hepslt_d1: Rlt (eps_ 1) d1.
rewrite the current goal using Hc1eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Hwlt: order_rel (setprod R R) w (d1,d2).
Apply (order_rel_setprod_R_R_intro (eps_ 1) (eps_ 1) d1 d2) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hepslt_d1.
We prove the intermediate claim Hwltb0: order_rel (setprod R R) w b0.
rewrite the current goal using HdPair (from right to left).
An exact proof term for the current goal is Hwlt.
We prove the intermediate claim Ha0RR: a0 ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R a0 Ha0Sq).
We prove the intermediate claim Hp0RR: p0 ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R p0 Hp0Sq).
We prove the intermediate claim HwRR: w ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R w HwSq).
We prove the intermediate claim Ha0w: order_rel (setprod R R) a0 w.
An exact proof term for the current goal is (order_rel_trans (setprod R R) a0 p0 w simply_ordered_set_setprod_R_R Ha0RR Hp0RR HwRR Ha0p0 Hp0w).
We prove the intermediate claim HwI: w ∈ I.
rewrite the current goal using HeqI (from left to right).
Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0) w HwSq) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0w.
An exact proof term for the current goal is Hwltb0.
We prove the intermediate claim HwU: w ∈ U.
An exact proof term for the current goal is (HIU w HwI).
We prove the intermediate claim HwUcap: w ∈ U ∩ ordsq_E.
An exact proof term for the current goal is (binintersectI U ordsq_E w HwU HwE).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_E) w HwUcap).
Assume Heq: c1 = d1 ∧ Rlt c2 d2.
We prove the intermediate claim Hd2pos: Rlt 0 d2.
rewrite the current goal using Hc2eq (from right to left) at position 1.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Heq).
We prove the intermediate claim Hb0proj1: proj1 b0 ∈ unit_interval.
An exact proof term for the current goal is (proj1_Sigma unit_interval (λ_ : set ⇒ unit_interval) b0 Hb0Sq).
We prove the intermediate claim Hb0_1U: b0 1 ∈ unit_interval.
rewrite the current goal using (proj1_ap_1 b0) (from right to left) at position 1.
An exact proof term for the current goal is Hb0proj1.
We prove the intermediate claim Hd2U: d2 ∈ unit_interval.
rewrite the current goal using Hd2eq (from left to right) at position 1.
An exact proof term for the current goal is Hb0_1U.
We prove the intermediate claim Hd2R: d2 ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R d2 Hd2U).
Apply (rational_dense_between_reals 0 d2 real_0 Hd2R Hd2pos) to the current goal.
Let q be given.
Assume Hqpack.
Apply Hqpack to the current goal.
Assume HqQ Hqconj.
Apply Hqconj to the current goal.
Assume H0ltq Hqltd2.
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 Hd2prop: ¬ (Rlt d2 0) ∧ ¬ (Rlt 1 d2).
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z 0) ∧ ¬ (Rlt 1 z)) d2 Hd2U).
We prove the intermediate claim Hnot1ltd2: ¬ (Rlt 1 d2).
An exact proof term for the current goal is (andER (¬ (Rlt d2 0)) (¬ (Rlt 1 d2)) Hd2prop).
We prove the intermediate claim Hqlt1: Rlt q 1.
Apply (xm (Rlt q 1)) to the current goal.
Assume Hq1: Rlt q 1.
An exact proof term for the current goal is Hq1.
Assume Hnq1: ¬ (Rlt q 1).
Apply FalseE to the current goal.
We prove the intermediate claim H1leq: Rle 1 q.
An exact proof term for the current goal is (RleI 1 q real_1 HqR Hnq1).
We prove the intermediate claim H1ltd2: Rlt 1 d2.
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid 1 q d2 H1leq Hqltd2).
An exact proof term for the current goal is (Hnot1ltd2 H1ltd2).
We prove the intermediate claim HqU: q ∈ unit_interval.
Apply (SepI R (λz : set ⇒ ¬ (Rlt z 0) ∧ ¬ (Rlt 1 z)) q HqR) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (not_Rlt_sym 0 q H0ltq).
An exact proof term for the current goal is (not_Rlt_sym q 1 Hqlt1).
Set w to be the term (eps_ 1,q).
We prove the intermediate claim HwSq: w ∈ ordered_square.
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 HqU).
We prove the intermediate claim HwE: w ∈ ordsq_E.
Apply (SepI ordered_square (λp0 : set ⇒ ∃y0 : set, p0 = (eps_ 1,y0) ∧ Rlt 0 y0 ∧ Rlt y0 1) w HwSq) to the current goal.
We use q to witness the existential quantifier.
We will prove w = (eps_ 1,q) ∧ Rlt 0 q ∧ Rlt q 1.
Apply andI to the current goal.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is H0ltq.
An exact proof term for the current goal is Hqlt1.
We prove the intermediate claim Hp0w: order_rel (setprod R R) p0 w.
Apply (order_rel_setprod_R_R_intro (eps_ 1) 0 (eps_ 1) q) 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 H0ltq.
We prove the intermediate claim Heps_eq_d1: (eps_ 1) = d1.
rewrite the current goal using Hc1eq (from right to left) at position 1.
An exact proof term for the current goal is (andEL (c1 = d1) (Rlt c2 d2) Heq).
We prove the intermediate claim Hwlt: order_rel (setprod R R) w (d1,d2).
Apply (order_rel_setprod_R_R_intro (eps_ 1) q d1 d2) to the current goal.
Apply orIR to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Heps_eq_d1.
An exact proof term for the current goal is Hqltd2.
We prove the intermediate claim Hwltb0: order_rel (setprod R R) w b0.
rewrite the current goal using HdPair (from right to left).
An exact proof term for the current goal is Hwlt.
We prove the intermediate claim Ha0RR: a0 ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R a0 Ha0Sq).
We prove the intermediate claim Hp0RR: p0 ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R p0 Hp0Sq).
We prove the intermediate claim HwRR: w ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R w HwSq).
We prove the intermediate claim Ha0w: order_rel (setprod R R) a0 w.
An exact proof term for the current goal is (order_rel_trans (setprod R R) a0 p0 w simply_ordered_set_setprod_R_R Ha0RR Hp0RR HwRR Ha0p0 Hp0w).
We prove the intermediate claim HwI: w ∈ I.
rewrite the current goal using HeqI (from left to right).
Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0) w HwSq) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0w.
An exact proof term for the current goal is Hwltb0.
We prove the intermediate claim HwU: w ∈ U.
An exact proof term for the current goal is (HIU w HwI).
We prove the intermediate claim HwUcap: w ∈ U ∩ ordsq_E.
An exact proof term for the current goal is (binintersectI U ordsq_E w HwU HwE).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_E) w HwUcap).
Assume HIlow: I ∈ Blow.
We prove the intermediate claim HIlow_ex: ∃b0 ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) x b0}.
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 b0 be given.
Assume Hb0pack.
Apply Hb0pack to the current goal.
Assume Hb0Sq HeqI.
We prove the intermediate claim Hp0I2: p0 ∈ {x ∈ ordered_square|order_rel (setprod R R) x b0}.
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 Hp0b0: order_rel (setprod R R) p0 b0.
An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) x0 b0) p0 Hp0I2).
We prove the intermediate claim Hcase: ∃c1 c2 d1 d2 : set, p0 = (c1,c2) ∧ b0 = (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 b0 Hp0b0).
Apply Hcase 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.
Apply Hcore to the current goal.
Assume Hab Hdisj.
Apply Hab to the current goal.
Assume Hp0Eq Hb0Eq.
We prove the intermediate claim Hp0def: p0 = (eps_ 1,0).
Use reflexivity.
We prove the intermediate claim HcPair: (c1,c2) = (eps_ 1,0).
rewrite the current goal using Hp0def (from right to left) at position 1.
rewrite the current goal using Hp0Eq (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hc1eq: c1 = (eps_ 1).
We will prove c1 = (eps_ 1).
rewrite the current goal using (tuple_2_0_eq c1 c2) (from right to left) at position 1.
rewrite the current goal using HcPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) 0).
We prove the intermediate claim Hc2eq: c2 = 0.
We will prove c2 = 0.
rewrite the current goal using (tuple_2_1_eq c1 c2) (from right to left) at position 1.
rewrite the current goal using HcPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq (eps_ 1) 0).
We prove the intermediate claim HdPair: (d1,d2) = b0.
rewrite the current goal using Hb0Eq (from right to left) at position 1.
Use reflexivity.
We prove the intermediate claim Hd1eq: d1 = (b0 0).
We will prove d1 = (b0 0).
rewrite the current goal using (tuple_2_0_eq d1 d2) (from right to left) at position 1.
rewrite the current goal using HdPair (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hd2eq: d2 = (b0 1).
We will prove d2 = (b0 1).
rewrite the current goal using (tuple_2_1_eq d1 d2) (from right to left) at position 1.
rewrite the current goal using HdPair (from left to right) at position 1.
Use reflexivity.
Apply Hdisj to the current goal.
Assume Hlt: Rlt c1 d1.
Set w to be the term (eps_ 1,eps_ 1).
We prove the intermediate claim HwE: w ∈ ordsq_E.
We prove the intermediate claim Hweq: w = (eps_ 1,eps_ 1).
Use reflexivity.
rewrite the current goal using Hweq (from left to right).
An exact proof term for the current goal is ordsq_eps1_eps1_in_E.
We prove the intermediate claim HwSq: w ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval (eps_ 1) (eps_ 1) eps_1_in_unit_interval eps_1_in_unit_interval).
We prove the intermediate claim Hepslt_d1: Rlt (eps_ 1) d1.
rewrite the current goal using Hc1eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Hwlt: order_rel (setprod R R) w (d1,d2).
Apply (order_rel_setprod_R_R_intro (eps_ 1) (eps_ 1) d1 d2) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hepslt_d1.
We prove the intermediate claim Hwltb0: order_rel (setprod R R) w b0.
rewrite the current goal using HdPair (from right to left).
An exact proof term for the current goal is Hwlt.
We prove the intermediate claim HwI: w ∈ I.
rewrite the current goal using HeqI (from left to right).
Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) x0 b0) w HwSq) to the current goal.
An exact proof term for the current goal is Hwltb0.
We prove the intermediate claim HwU: w ∈ U.
An exact proof term for the current goal is (HIU w HwI).
We prove the intermediate claim HwUcap: w ∈ U ∩ ordsq_E.
An exact proof term for the current goal is (binintersectI U ordsq_E w HwU HwE).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_E) w HwUcap).
Assume Heq: c1 = d1 ∧ Rlt c2 d2.
We prove the intermediate claim Hd2pos: Rlt 0 d2.
rewrite the current goal using Hc2eq (from right to left) at position 1.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Heq).
We prove the intermediate claim Hb0proj1: proj1 b0 ∈ unit_interval.
An exact proof term for the current goal is (proj1_Sigma unit_interval (λ_ : set ⇒ unit_interval) b0 Hb0Sq).
We prove the intermediate claim Hb0_1U: b0 1 ∈ unit_interval.
rewrite the current goal using (proj1_ap_1 b0) (from right to left) at position 1.
An exact proof term for the current goal is Hb0proj1.
We prove the intermediate claim Hd2U: d2 ∈ unit_interval.
rewrite the current goal using Hd2eq (from left to right) at position 1.
An exact proof term for the current goal is Hb0_1U.
We prove the intermediate claim Hd2R: d2 ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R d2 Hd2U).
Apply (rational_dense_between_reals 0 d2 real_0 Hd2R Hd2pos) to the current goal.
Let q be given.
Assume Hqpack.
Apply Hqpack to the current goal.
Assume HqQ Hqconj.
Apply Hqconj to the current goal.
Assume H0ltq Hqltd2.
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 Hd2prop: ¬ (Rlt d2 0) ∧ ¬ (Rlt 1 d2).
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z 0) ∧ ¬ (Rlt 1 z)) d2 Hd2U).
We prove the intermediate claim Hnot1ltd2: ¬ (Rlt 1 d2).
An exact proof term for the current goal is (andER (¬ (Rlt d2 0)) (¬ (Rlt 1 d2)) Hd2prop).
We prove the intermediate claim Hd2le1: Rle d2 1.
An exact proof term for the current goal is (RleI d2 1 Hd2R real_1 Hnot1ltd2).
We prove the intermediate claim Hqlt1: Rlt q 1.
Apply (xm (Rlt q 1)) to the current goal.
Assume Hq1: Rlt q 1.
An exact proof term for the current goal is Hq1.
Assume Hnq1: ¬ (Rlt q 1).
Apply FalseE to the current goal.
We prove the intermediate claim H1leq: Rle 1 q.
An exact proof term for the current goal is (RleI 1 q real_1 HqR Hnq1).
We prove the intermediate claim H1ltd2: Rlt 1 d2.
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid 1 q d2 H1leq Hqltd2).
An exact proof term for the current goal is (Hnot1ltd2 H1ltd2).
We prove the intermediate claim HqU: q ∈ unit_interval.
Apply (SepI R (λz : set ⇒ ¬ (Rlt z 0) ∧ ¬ (Rlt 1 z)) q HqR) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (not_Rlt_sym 0 q H0ltq).
An exact proof term for the current goal is (not_Rlt_sym q 1 Hqlt1).
Set w to be the term (eps_ 1,q).
We prove the intermediate claim HwSq: w ∈ ordered_square.
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 HqU).
We prove the intermediate claim HwE: w ∈ ordsq_E.
Apply (SepI ordered_square (λp0 : set ⇒ ∃y0 : set, p0 = (eps_ 1,y0) ∧ Rlt 0 y0 ∧ Rlt y0 1) w HwSq) to the current goal.
We use q to witness the existential quantifier.
We will prove w = (eps_ 1,q) ∧ Rlt 0 q ∧ Rlt q 1.
Apply andI to the current goal.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is H0ltq.
An exact proof term for the current goal is Hqlt1.
We prove the intermediate claim Heps_eq_d1: (eps_ 1) = d1.
rewrite the current goal using Hc1eq (from right to left) at position 1.
An exact proof term for the current goal is (andEL (c1 = d1) (Rlt c2 d2) Heq).
We prove the intermediate claim Hwlt: order_rel (setprod R R) w (d1,d2).
Apply (order_rel_setprod_R_R_intro (eps_ 1) q d1 d2) to the current goal.
Apply orIR to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Heps_eq_d1.
An exact proof term for the current goal is Hqltd2.
We prove the intermediate claim Hwltb0: order_rel (setprod R R) w b0.
rewrite the current goal using HdPair (from right to left).
An exact proof term for the current goal is Hwlt.
We prove the intermediate claim HwI: w ∈ I.
rewrite the current goal using HeqI (from left to right).
Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) x0 b0) w HwSq) to the current goal.
An exact proof term for the current goal is Hwltb0.
We prove the intermediate claim HwU: w ∈ U.
An exact proof term for the current goal is (HIU w HwI).
We prove the intermediate claim HwUcap: w ∈ U ∩ ordsq_E.
An exact proof term for the current goal is (binintersectI U ordsq_E w HwU HwE).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_E) w HwUcap).
Assume HIup: I ∈ Bup.
We prove the intermediate claim HIup_ex: ∃a0 ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) a0 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 a0 be given.
Assume Ha0pack.
Apply Ha0pack to the current goal.
Assume Ha0Sq HeqI.
Set w to be the term (eps_ 1,eps_ 1).
We prove the intermediate claim HwE: w ∈ ordsq_E.
We prove the intermediate claim Hweq: w = (eps_ 1,eps_ 1).
Use reflexivity.
rewrite the current goal using Hweq (from left to right).
An exact proof term for the current goal is ordsq_eps1_eps1_in_E.
We prove the intermediate claim HwSq: w ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval (eps_ 1) (eps_ 1) eps_1_in_unit_interval eps_1_in_unit_interval).
We prove the intermediate claim Hp0w: order_rel (setprod R R) p0 w.
Apply (order_rel_setprod_R_R_intro (eps_ 1) 0 (eps_ 1) (eps_ 1)) 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 eps_1_pos_R.
We prove the intermediate claim Ha0p0: order_rel (setprod R R) a0 p0.
We prove the intermediate claim Hp0I2: p0 ∈ {x ∈ ordered_square|order_rel (setprod R R) a0 x}.
rewrite the current goal using HeqI (from right to left).
An exact proof term for the current goal is Hp0I.
An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0) p0 Hp0I2).
We prove the intermediate claim Ha0RR: a0 ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R a0 Ha0Sq).
We prove the intermediate claim Hp0RR: p0 ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R p0 Hp0Sq).
We prove the intermediate claim HwRR: w ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R w HwSq).
We prove the intermediate claim Ha0w: order_rel (setprod R R) a0 w.
An exact proof term for the current goal is (order_rel_trans (setprod R R) a0 p0 w simply_ordered_set_setprod_R_R Ha0RR Hp0RR HwRR Ha0p0 Hp0w).
We prove the intermediate claim HwI: w ∈ I.
rewrite the current goal using HeqI (from left to right).
Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0) w HwSq) to the current goal.
An exact proof term for the current goal is Ha0w.
We prove the intermediate claim Hwcap: w ∈ I ∩ ordsq_E.
An exact proof term for the current goal is (binintersectI I ordsq_E w HwI HwE).
We prove the intermediate claim HwU: w ∈ U.
An exact proof term for the current goal is (HIU w HwI).
We prove the intermediate claim HwUcap: w ∈ U ∩ ordsq_E.
An exact proof term for the current goal is (binintersectI U ordsq_E w HwU HwE).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_E) w HwUcap).
Assume Hp1: p ∈ {(eps_ 1,1)}.
We prove the intermediate claim HpEq: p = (eps_ 1,1).
An exact proof term for the current goal is (SingE (eps_ 1,1) p Hp1).
rewrite the current goal using HpEq (from left to right).
Set p1 to be the term (eps_ 1,1).
We prove the intermediate claim Hp1Sq: p1 ∈ 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 Hdefcl: closure_of ordered_square ordered_square_topology ordsq_E = {x ∈ ordered_square|∀U : set, U ∈ ordered_square_topology → x ∈ U → U ∩ ordsq_E ≠ Empty}.
Use reflexivity.
rewrite the current goal using Hdefcl (from left to right).
Apply (SepI ordered_square (λx0 : set ⇒ ∀U : set, U ∈ ordered_square_topology → x0 ∈ U → U ∩ ordsq_E ≠ Empty) p1 Hp1Sq) to the current goal.
Let U be given.
Assume HUtop: U ∈ ordered_square_topology.
Assume Hp1U: p1 ∈ U.
We will prove U ∩ ordsq_E ≠ Empty.
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 HUtop.
We prove the intermediate claim HexI: ∃I ∈ ordered_square_order_basis, p1 ∈ I ∧ I ⊆ U.
An exact proof term for the current goal is (generated_topology_local_refine ordered_square ordered_square_order_basis U p1 HUgt Hp1U).
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 Hp1I HIU.
Set Bint to be the term {J ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, J = {x ∈ ordered_square|order_rel (setprod R R) a0 x ∧ order_rel (setprod R R) x b0}}.
Set Blow to be the term {J ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, J = {x ∈ ordered_square|order_rel (setprod R R) x b0}}.
Set Bup to be the term {J ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, J = {x ∈ ordered_square|order_rel (setprod R R) a0 x}}.
We prove the intermediate claim HIcase: I ∈ ((Bint ∪ Blow) ∪ Bup).
We prove the intermediate claim HdefB: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).
Use reflexivity.
rewrite the current goal using HdefB (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: ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) a0 x ∧ order_rel (setprod R R) x b0}.
An exact proof term for the current goal is (SepE2 (𝒫 ordered_square) (λJ0 : set ⇒ ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, J0 = {x ∈ ordered_square|order_rel (setprod R R) a0 x ∧ order_rel (setprod R R) x b0}) I HIint).
Apply HIint_ex to the current goal.
Let a0 be given.
Assume Ha0rest.
Apply Ha0rest to the current goal.
Assume Ha0Sq Hb0core.
Apply Hb0core to the current goal.
Let b0 be given.
Assume Hb0rest.
Apply Hb0rest to the current goal.
Assume Hb0Sq HeqI.
We prove the intermediate claim Hp1I2: p1 ∈ {x ∈ ordered_square|order_rel (setprod R R) a0 x ∧ order_rel (setprod R R) x b0}.
rewrite the current goal using HeqI (from right to left).
An exact proof term for the current goal is Hp1I.
We prove the intermediate claim Hp1props: order_rel (setprod R R) a0 p1 ∧ order_rel (setprod R R) p1 b0.
An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0) p1 Hp1I2).
Apply Hp1props to the current goal.
Assume Ha0p1 Hp1b0.
We prove the intermediate claim Hcase: ∃c1 c2 d1 d2 : set, a0 = (c1,c2) ∧ p1 = (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 a0 p1 Ha0p1).
Apply Hcase 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.
Apply Hcore to the current goal.
Assume Hab Hdisj.
Apply Hab to the current goal.
Assume Ha0Eq Hp1Eq.
We prove the intermediate claim Hp1def: p1 = (eps_ 1,1).
Use reflexivity.
We prove the intermediate claim HdPair: (d1,d2) = (eps_ 1,1).
rewrite the current goal using Hp1def (from right to left) at position 1.
rewrite the current goal using Hp1Eq (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hd1eq: d1 = (eps_ 1).
We will prove d1 = (eps_ 1).
rewrite the current goal using (tuple_2_0_eq d1 d2) (from right to left) at position 1.
rewrite the current goal using HdPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) 1).
We prove the intermediate claim Hd2eq: d2 = 1.
We will prove d2 = 1.
rewrite the current goal using (tuple_2_1_eq d1 d2) (from right to left) at position 1.
rewrite the current goal using HdPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq (eps_ 1) 1).
Apply Hdisj to the current goal.
Assume Hlt: Rlt c1 d1.
Set w to be the term (eps_ 1,eps_ 1).
We prove the intermediate claim HwE: w ∈ ordsq_E.
We prove the intermediate claim Hweq: w = (eps_ 1,eps_ 1).
Use reflexivity.
rewrite the current goal using Hweq (from left to right).
An exact proof term for the current goal is ordsq_eps1_eps1_in_E.
We prove the intermediate claim HwSq: w ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval (eps_ 1) (eps_ 1) eps_1_in_unit_interval eps_1_in_unit_interval).
We prove the intermediate claim Ha0w: order_rel (setprod R R) a0 w.
rewrite the current goal using Ha0Eq (from left to right) at position 1.
Apply (order_rel_setprod_R_R_intro c1 c2 (eps_ 1) (eps_ 1)) to the current goal.
Apply orIL to the current goal.
We prove the intermediate claim Hc1lt: Rlt c1 (eps_ 1).
rewrite the current goal using Hd1eq (from right to left).
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is Hc1lt.
We prove the intermediate claim Hwp1: order_rel (setprod R R) w p1.
Apply (order_rel_setprod_R_R_intro (eps_ 1) (eps_ 1) (eps_ 1) 1) 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 eps_1_lt1_R.
We prove the intermediate claim Ha0RR: a0 ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R a0 Ha0Sq).
We prove the intermediate claim Hp1RR: p1 ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R p1 Hp1Sq).
We prove the intermediate claim HwRR: w ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R w HwSq).
We prove the intermediate claim Hb0RR: b0 ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R b0 Hb0Sq).
We prove the intermediate claim Hwb0: order_rel (setprod R R) w b0.
An exact proof term for the current goal is (order_rel_trans (setprod R R) w p1 b0 simply_ordered_set_setprod_R_R HwRR Hp1RR Hb0RR Hwp1 Hp1b0).
We prove the intermediate claim HwI: w ∈ I.
rewrite the current goal using HeqI (from left to right).
Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0) w HwSq) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0w.
An exact proof term for the current goal is Hwb0.
We prove the intermediate claim HwU: w ∈ U.
An exact proof term for the current goal is (HIU w HwI).
We prove the intermediate claim HwUcap: w ∈ U ∩ ordsq_E.
An exact proof term for the current goal is (binintersectI U ordsq_E w HwU HwE).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_E) w HwUcap).
Assume Heq: c1 = d1 ∧ Rlt c2 d2.
We prove the intermediate claim Hc2lt1: Rlt c2 1.
rewrite the current goal using Hd2eq (from right to left).
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Heq).
We prove the intermediate claim Ha0proj1: proj1 a0 ∈ unit_interval.
An exact proof term for the current goal is (proj1_Sigma unit_interval (λ_ : set ⇒ unit_interval) a0 Ha0Sq).
We prove the intermediate claim Ha0_1U: a0 1 ∈ unit_interval.
rewrite the current goal using (proj1_ap_1 a0) (from right to left) at position 1.
An exact proof term for the current goal is Ha0proj1.
We prove the intermediate claim Hc2eq: c2 = (a0 1).
We will prove c2 = (a0 1).
rewrite the current goal using (tuple_2_1_eq c1 c2) (from right to left) at position 1.
rewrite the current goal using Ha0Eq (from right to left) at position 1.
Use reflexivity.
We prove the intermediate claim Hc2U: c2 ∈ unit_interval.
rewrite the current goal using Hc2eq (from left to right) at position 1.
An exact proof term for the current goal is Ha0_1U.
We prove the intermediate claim Hc2R: c2 ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R c2 Hc2U).
Apply (rational_dense_between_reals c2 1 Hc2R real_1 Hc2lt1) to the current goal.
Let q be given.
Assume Hqpack.
Apply Hqpack to the current goal.
Assume HqQ Hqconj.
Apply Hqconj to the current goal.
Assume Hc2ltq Hqlt1.
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 Hc2prop: ¬ (Rlt c2 0) ∧ ¬ (Rlt 1 c2).
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z 0) ∧ ¬ (Rlt 1 z)) c2 Hc2U).
We prove the intermediate claim Hnotc2lt0: ¬ (Rlt c2 0).
An exact proof term for the current goal is (andEL (¬ (Rlt c2 0)) (¬ (Rlt 1 c2)) Hc2prop).
We prove the intermediate claim H0lec2: Rle 0 c2.
An exact proof term for the current goal is (RleI 0 c2 real_0 Hc2R Hnotc2lt0).
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid 0 c2 q H0lec2 Hc2ltq).
We prove the intermediate claim HqU: q ∈ unit_interval.
Apply (SepI R (λz : set ⇒ ¬ (Rlt z 0) ∧ ¬ (Rlt 1 z)) q HqR) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (not_Rlt_sym 0 q H0ltq).
An exact proof term for the current goal is (not_Rlt_sym q 1 Hqlt1).
Set w to be the term (eps_ 1,q).
We prove the intermediate claim HwSq: w ∈ ordered_square.
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 HqU).
We prove the intermediate claim HwE: w ∈ ordsq_E.
Apply (SepI ordered_square (λp0 : set ⇒ ∃y0 : set, p0 = (eps_ 1,y0) ∧ Rlt 0 y0 ∧ Rlt y0 1) w HwSq) to the current goal.
We use q to witness the existential quantifier.
We will prove w = (eps_ 1,q) ∧ Rlt 0 q ∧ Rlt q 1.
Apply andI to the current goal.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is H0ltq.
An exact proof term for the current goal is Hqlt1.
We prove the intermediate claim Ha0w: order_rel (setprod R R) a0 w.
rewrite the current goal using Ha0Eq (from left to right) at position 1.
Apply (order_rel_setprod_R_R_intro c1 c2 (eps_ 1) q) to the current goal.
Apply orIR to the current goal.
Apply andI to the current goal.
rewrite the current goal using Hd1eq (from right to left).
An exact proof term for the current goal is (andEL (c1 = d1) (Rlt c2 d2) Heq).
An exact proof term for the current goal is Hc2ltq.
We prove the intermediate claim Hwp1: order_rel (setprod R R) w p1.
Apply (order_rel_setprod_R_R_intro (eps_ 1) q (eps_ 1) 1) 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 Hqlt1.
We prove the intermediate claim Ha0RR: a0 ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R a0 Ha0Sq).
We prove the intermediate claim Hp1RR: p1 ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R p1 Hp1Sq).
We prove the intermediate claim HwRR: w ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R w HwSq).
We prove the intermediate claim Hb0RR: b0 ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R b0 Hb0Sq).
We prove the intermediate claim Hwb0: order_rel (setprod R R) w b0.
An exact proof term for the current goal is (order_rel_trans (setprod R R) w p1 b0 simply_ordered_set_setprod_R_R HwRR Hp1RR Hb0RR Hwp1 Hp1b0).
We prove the intermediate claim HwI: w ∈ I.
rewrite the current goal using HeqI (from left to right).
Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0) w HwSq) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0w.
An exact proof term for the current goal is Hwb0.
We prove the intermediate claim HwU: w ∈ U.
An exact proof term for the current goal is (HIU w HwI).
We prove the intermediate claim HwUcap: w ∈ U ∩ ordsq_E.
An exact proof term for the current goal is (binintersectI U ordsq_E w HwU HwE).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_E) w HwUcap).
Assume HIlow: I ∈ Blow.
We prove the intermediate claim HIlow_ex: ∃b0 ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) x b0}.
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 b0 be given.
Assume Hb0pack.
Apply Hb0pack to the current goal.
Assume Hb0Sq HeqI.
We prove the intermediate claim Hp1I2: p1 ∈ {x ∈ ordered_square|order_rel (setprod R R) x b0}.
rewrite the current goal using HeqI (from right to left).
An exact proof term for the current goal is Hp1I.
We prove the intermediate claim Hp1b0: order_rel (setprod R R) p1 b0.
An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) x0 b0) p1 Hp1I2).
Set w to be the term (eps_ 1,eps_ 1).
We prove the intermediate claim HwE: w ∈ ordsq_E.
We prove the intermediate claim Hweq: w = (eps_ 1,eps_ 1).
Use reflexivity.
rewrite the current goal using Hweq (from left to right).
An exact proof term for the current goal is ordsq_eps1_eps1_in_E.
We prove the intermediate claim HwSq: w ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval (eps_ 1) (eps_ 1) eps_1_in_unit_interval eps_1_in_unit_interval).
We prove the intermediate claim Hwp1: order_rel (setprod R R) w p1.
Apply (order_rel_setprod_R_R_intro (eps_ 1) (eps_ 1) (eps_ 1) 1) 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 eps_1_lt1_R.
We prove the intermediate claim HwRR: w ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R w HwSq).
We prove the intermediate claim Hp1RR: p1 ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R p1 Hp1Sq).
We prove the intermediate claim Hb0RR: b0 ∈ setprod R R.
An exact proof term for the current goal is (ordered_square_sub_setprod_R_R b0 Hb0Sq).
We prove the intermediate claim Hwb0: order_rel (setprod R R) w b0.
An exact proof term for the current goal is (order_rel_trans (setprod R R) w p1 b0 simply_ordered_set_setprod_R_R HwRR Hp1RR Hb0RR Hwp1 Hp1b0).
We prove the intermediate claim HwI: w ∈ I.
rewrite the current goal using HeqI (from left to right).
Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) x0 b0) w HwSq) to the current goal.
An exact proof term for the current goal is Hwb0.
We prove the intermediate claim HwU: w ∈ U.
An exact proof term for the current goal is (HIU w HwI).
We prove the intermediate claim HwUcap: w ∈ U ∩ ordsq_E.
An exact proof term for the current goal is (binintersectI U ordsq_E w HwU HwE).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_E) w HwUcap).
Assume HIup: I ∈ Bup.
We prove the intermediate claim HIup_ex: ∃a0 ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) a0 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 a0 be given.
Assume Ha0pack.
Apply Ha0pack to the current goal.
Assume Ha0Sq HeqI.
We prove the intermediate claim Hp1I2: p1 ∈ {x ∈ ordered_square|order_rel (setprod R R) a0 x}.
rewrite the current goal using HeqI (from right to left).
An exact proof term for the current goal is Hp1I.
We prove the intermediate claim Ha0p1: order_rel (setprod R R) a0 p1.
An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0) p1 Hp1I2).
We prove the intermediate claim Hcase: ∃c1 c2 d1 d2 : set, a0 = (c1,c2) ∧ p1 = (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 a0 p1 Ha0p1).
Apply Hcase 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.
Apply Hcore to the current goal.
Assume Hab Hdisj.
Apply Hab to the current goal.
Assume Ha0Eq Hp1Eq.
We prove the intermediate claim Hp1def: p1 = (eps_ 1,1).
Use reflexivity.
We prove the intermediate claim HdPair: (d1,d2) = (eps_ 1,1).
rewrite the current goal using Hp1def (from right to left) at position 1.
rewrite the current goal using Hp1Eq (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hd1eq: d1 = (eps_ 1).
We will prove d1 = (eps_ 1).
rewrite the current goal using (tuple_2_0_eq d1 d2) (from right to left) at position 1.
rewrite the current goal using HdPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_0_eq (eps_ 1) 1).
We prove the intermediate claim Hd2eq: d2 = 1.
We will prove d2 = 1.
rewrite the current goal using (tuple_2_1_eq d1 d2) (from right to left) at position 1.
rewrite the current goal using HdPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq (eps_ 1) 1).
Apply Hdisj to the current goal.
Assume Hlt: Rlt c1 d1.
Set w to be the term (eps_ 1,eps_ 1).
We prove the intermediate claim HwE: w ∈ ordsq_E.
We prove the intermediate claim Hweq: w = (eps_ 1,eps_ 1).
Use reflexivity.
rewrite the current goal using Hweq (from left to right).
An exact proof term for the current goal is ordsq_eps1_eps1_in_E.
We prove the intermediate claim HwSq: w ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval (eps_ 1) (eps_ 1) eps_1_in_unit_interval eps_1_in_unit_interval).
We prove the intermediate claim Ha0w: order_rel (setprod R R) a0 w.
rewrite the current goal using Ha0Eq (from left to right) at position 1.
Apply (order_rel_setprod_R_R_intro c1 c2 (eps_ 1) (eps_ 1)) to the current goal.
Apply orIL to the current goal.
We prove the intermediate claim Hc1lt: Rlt c1 (eps_ 1).
rewrite the current goal using Hd1eq (from right to left).
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is Hc1lt.
We prove the intermediate claim Hwp1: order_rel (setprod R R) w p1.
Apply (order_rel_setprod_R_R_intro (eps_ 1) (eps_ 1) (eps_ 1) 1) 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 eps_1_lt1_R.
We prove the intermediate claim HwI: w ∈ I.
rewrite the current goal using HeqI (from left to right).
Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0) w HwSq) to the current goal.
An exact proof term for the current goal is Ha0w.
We prove the intermediate claim HwU: w ∈ U.
An exact proof term for the current goal is (HIU w HwI).
We prove the intermediate claim HwUcap: w ∈ U ∩ ordsq_E.
An exact proof term for the current goal is (binintersectI U ordsq_E w HwU HwE).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_E) w HwUcap).
Assume Heq: c1 = d1 ∧ Rlt c2 d2.
We prove the intermediate claim Hc2lt1: Rlt c2 1.
rewrite the current goal using Hd2eq (from right to left).
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Heq).
We prove the intermediate claim Ha0proj1: proj1 a0 ∈ unit_interval.
An exact proof term for the current goal is (proj1_Sigma unit_interval (λ_ : set ⇒ unit_interval) a0 Ha0Sq).
We prove the intermediate claim Ha0_1U: a0 1 ∈ unit_interval.
rewrite the current goal using (proj1_ap_1 a0) (from right to left) at position 1.
An exact proof term for the current goal is Ha0proj1.
We prove the intermediate claim Hc2eq: c2 = (a0 1).
We will prove c2 = (a0 1).
rewrite the current goal using (tuple_2_1_eq c1 c2) (from right to left) at position 1.
rewrite the current goal using Ha0Eq (from right to left) at position 1.
Use reflexivity.
We prove the intermediate claim Hc2U: c2 ∈ unit_interval.
rewrite the current goal using Hc2eq (from left to right) at position 1.
An exact proof term for the current goal is Ha0_1U.
We prove the intermediate claim Hc2R: c2 ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R c2 Hc2U).
Apply (rational_dense_between_reals c2 1 Hc2R real_1 Hc2lt1) to the current goal.
Let q be given.
Assume Hqpack.
Apply Hqpack to the current goal.
Assume HqQ Hqconj.
Apply Hqconj to the current goal.
Assume Hc2ltq Hqlt1.
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 Hc2prop: ¬ (Rlt c2 0) ∧ ¬ (Rlt 1 c2).
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z 0) ∧ ¬ (Rlt 1 z)) c2 Hc2U).
We prove the intermediate claim Hnotc2lt0: ¬ (Rlt c2 0).
An exact proof term for the current goal is (andEL (¬ (Rlt c2 0)) (¬ (Rlt 1 c2)) Hc2prop).
We prove the intermediate claim H0lec2: Rle 0 c2.
An exact proof term for the current goal is (RleI 0 c2 real_0 Hc2R Hnotc2lt0).
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid 0 c2 q H0lec2 Hc2ltq).
We prove the intermediate claim HqU: q ∈ unit_interval.
Apply (SepI R (λz : set ⇒ ¬ (Rlt z 0) ∧ ¬ (Rlt 1 z)) q HqR) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (not_Rlt_sym 0 q H0ltq).
An exact proof term for the current goal is (not_Rlt_sym q 1 Hqlt1).
Set w to be the term (eps_ 1,q).
We prove the intermediate claim HwSq: w ∈ ordered_square.
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 HqU).
We prove the intermediate claim HwE: w ∈ ordsq_E.
Apply (SepI ordered_square (λp0 : set ⇒ ∃y0 : set, p0 = (eps_ 1,y0) ∧ Rlt 0 y0 ∧ Rlt y0 1) w HwSq) to the current goal.
We use q to witness the existential quantifier.
We will prove w = (eps_ 1,q) ∧ Rlt 0 q ∧ Rlt q 1.
Apply andI to the current goal.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is H0ltq.
An exact proof term for the current goal is Hqlt1.
We prove the intermediate claim Ha0w: order_rel (setprod R R) a0 w.
rewrite the current goal using Ha0Eq (from left to right) at position 1.
Apply (order_rel_setprod_R_R_intro c1 c2 (eps_ 1) q) to the current goal.
Apply orIR to the current goal.
Apply andI to the current goal.
rewrite the current goal using Hd1eq (from right to left).
An exact proof term for the current goal is (andEL (c1 = d1) (Rlt c2 d2) Heq).
An exact proof term for the current goal is Hc2ltq.
We prove the intermediate claim HwI: w ∈ I.
rewrite the current goal using HeqI (from left to right).
Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0) w HwSq) to the current goal.
An exact proof term for the current goal is Ha0w.
We prove the intermediate claim HwU: w ∈ U.
An exact proof term for the current goal is (HIU w HwI).
We prove the intermediate claim HwUcap: w ∈ U ∩ ordsq_E.
An exact proof term for the current goal is (binintersectI U ordsq_E w HwU HwE).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_E) w HwUcap).
∎