Let p be given.
Assume HpTop: p ∈ ordsq_top_edge_lt1.
We will prove p ∈ closure_of ordered_square ordered_square_topology ordsq_D.
We prove the intermediate claim HpSq: p ∈ ordered_square.
An exact proof term for the current goal is (SepE1 ordered_square (λp0 : set ⇒ ∃x : set, p0 = (x,1) ∧ x ∈ unit_interval ∧ Rlt x 1) p HpTop).
We prove the intermediate claim Hexx: ∃x : set, p = (x,1) ∧ x ∈ unit_interval ∧ Rlt x 1.
An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃x : set, p0 = (x,1) ∧ x ∈ unit_interval ∧ Rlt x 1) p HpTop).
Apply Hexx to the current goal.
Let x be given.
Assume Hxpack.
We prove the intermediate claim Hxcore: p = (x,1) ∧ x ∈ unit_interval.
An exact proof term for the current goal is (andEL (p = (x,1) ∧ x ∈ unit_interval) (Rlt x 1) Hxpack).
We prove the intermediate claim Hxlt1: Rlt x 1.
An exact proof term for the current goal is (andER (p = (x,1) ∧ x ∈ unit_interval) (Rlt x 1) Hxpack).
We prove the intermediate claim HpEq: p = (x,1).
An exact proof term for the current goal is (andEL (p = (x,1)) (x ∈ unit_interval) Hxcore).
We prove the intermediate claim HxU: x ∈ unit_interval.
An exact proof term for the current goal is (andER (p = (x,1)) (x ∈ unit_interval) Hxcore).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R x HxU).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim Hxnotlt0: ¬ (Rlt x 0).
An exact proof term for the current goal is (andEL (¬ (Rlt x 0)) (¬ (Rlt 1 x)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) x HxU)).
We prove the intermediate claim Hxle0: Rle 0 x.
An exact proof term for the current goal is (RleI 0 x real_0 HxR Hxnotlt0).
We prove the intermediate claim Hdefcl: closure_of ordered_square ordered_square_topology ordsq_D = {x0 ∈ ordered_square|∀U : set, U ∈ ordered_square_topology → x0 ∈ U → U ∩ ordsq_D ≠ 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_D ≠ Empty) p HpSq) to the current goal.
Let U be given.
Assume HUtop: U ∈ ordered_square_topology.
Assume HpU: p ∈ U.
We will prove U ∩ ordsq_D ≠ Empty.
We prove the intermediate claim HexI: ∃I ∈ ordered_square_order_basis, p ∈ I ∧ I ⊆ U.
An exact proof term for the current goal is (generated_topology_local_refine ordered_square ordered_square_order_basis U p HUtop HpU).
Apply HexI to the current goal.
Let I be given.
Assume HIpack.
Apply HIpack to the current goal.
Assume HIbas HIcore.
Apply HIcore to the current goal.
Assume HpI HIU.
Set Bint to be the term {J ∈ 𝒫 ordered_square|∃a ∈ ordered_square, ∃b ∈ ordered_square, J = {z ∈ ordered_square|order_rel (setprod R R) a z ∧ order_rel (setprod R R) z b}}.
Set Blow to be the term {J ∈ 𝒫 ordered_square|∃b ∈ ordered_square, J = {z ∈ ordered_square|order_rel (setprod R R) z b}}.
Set Bup to be the term {J ∈ 𝒫 ordered_square|∃a ∈ ordered_square, J = {z ∈ ordered_square|order_rel (setprod R R) a z}}.
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 Hexab: ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {z ∈ ordered_square|order_rel (setprod R R) a0 z ∧ order_rel (setprod R R) z b0}.
An exact proof term for the current goal is (SepE2 (𝒫 ordered_square) (λJ0 : set ⇒ ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, J0 = {z ∈ ordered_square|order_rel (setprod R R) a0 z ∧ order_rel (setprod R R) z b0}) I HIint).
Apply Hexab to the current goal.
Let a0 be given.
Assume Ha0pack.
Apply Ha0pack to the current goal.
Assume Ha0Sq Hb0ex.
Apply Hb0ex to the current goal.
Let b0 be given.
Assume Hb0pack.
Apply Hb0pack to the current goal.
Assume Hb0Sq HIeq.
We prove the intermediate claim HpI': p ∈ {z ∈ ordered_square|order_rel (setprod R R) a0 z ∧ order_rel (setprod R R) z b0}.
rewrite the current goal using HIeq (from right to left).
An exact proof term for the current goal is HpI.
We prove the intermediate claim HpCore: order_rel (setprod R R) a0 p ∧ order_rel (setprod R R) p b0.
An exact proof term for the current goal is (SepE2 ordered_square (λz : set ⇒ order_rel (setprod R R) a0 z ∧ order_rel (setprod R R) z b0) p HpI').
We prove the intermediate claim Ha0p: order_rel (setprod R R) a0 p.
An exact proof term for the current goal is (andEL (order_rel (setprod R R) a0 p) (order_rel (setprod R R) p b0) HpCore).
We prove the intermediate claim Hpb0: order_rel (setprod R R) p b0.
An exact proof term for the current goal is (andER (order_rel (setprod R R) a0 p) (order_rel (setprod R R) p b0) HpCore).
Set b00 to be the term b0 0.
Set b01 to be the term b0 1.
We prove the intermediate claim Hb00U: b00 ∈ unit_interval.
An exact proof term for the current goal is (ap0_Sigma unit_interval (λ_ : set ⇒ unit_interval) b0 Hb0Sq).
We prove the intermediate claim Hb01U: b01 ∈ unit_interval.
An exact proof term for the current goal is (ap1_Sigma unit_interval (λ_ : set ⇒ unit_interval) b0 Hb0Sq).
We prove the intermediate claim Hb00R: b00 ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R b00 Hb00U).
We prove the intermediate claim Hb00S: SNo b00.
An exact proof term for the current goal is (real_SNo b00 Hb00R).
We prove the intermediate claim Hb01not1: ¬ (Rlt 1 b01).
An exact proof term for the current goal is (andER (¬ (Rlt b01 0)) (¬ (Rlt 1 b01)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) b01 Hb01U)).
We prove the intermediate claim Hxltb00: Rlt x b00.
We prove the intermediate claim Hb0Eta: b0 = (b00,b01).
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval b0 Hb0Sq).
We prove the intermediate claim Hunf: ∃c1 c2 d1 d2 : set, p = (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 p b0 Hpb0).
Apply Hunf 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 Hcore2.
Apply Hcore2 to the current goal.
Assume Hab Hdisj.
Apply Hab to the current goal.
Assume HpEq2 HbEq2.
We prove the intermediate claim HpPair: (c1,c2) = (x,1).
We will prove (c1,c2) = (x,1).
rewrite the current goal using HpEq (from right to left).
rewrite the current goal using HpEq2 (from right to left).
Use reflexivity.
We prove the intermediate claim Hccoords: c1 = x ∧ c2 = 1.
An exact proof term for the current goal is (tuple_eq_coords c1 c2 x 1 HpPair).
We prove the intermediate claim Hc1eq: c1 = x.
An exact proof term for the current goal is (andEL (c1 = x) (c2 = 1) Hccoords).
We prove the intermediate claim Hc2eq: c2 = 1.
An exact proof term for the current goal is (andER (c1 = x) (c2 = 1) Hccoords).
We prove the intermediate claim HbPair: (d1,d2) = (b00,b01).
We will prove (d1,d2) = (b00,b01).
rewrite the current goal using Hb0Eta (from right to left).
rewrite the current goal using HbEq2 (from right to left).
Use reflexivity.
We prove the intermediate claim Hdcoords: d1 = b00 ∧ d2 = b01.
An exact proof term for the current goal is (tuple_eq_coords d1 d2 b00 b01 HbPair).
We prove the intermediate claim Hd1eq: d1 = b00.
An exact proof term for the current goal is (andEL (d1 = b00) (d2 = b01) Hdcoords).
We prove the intermediate claim Hd2eq: d2 = b01.
An exact proof term for the current goal is (andER (d1 = b00) (d2 = b01) Hdcoords).
Apply Hdisj 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).
An exact proof term for the current goal is Hlt.
Assume Heq: c1 = d1 ∧ Rlt c2 d2.
Apply FalseE to the current goal.
We prove the intermediate claim H1ltb01: Rlt 1 b01.
rewrite the current goal using Hc2eq (from right to left) at position 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).
An exact proof term for the current goal is (Hb01not1 H1ltb01).
Apply (rational_dense_between_reals x b00 HxR Hb00R Hxltb00) to the current goal.
Let q be given.
Assume Hqpack.
Apply Hqpack 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 Hxltq: Rlt x q.
An exact proof term for the current goal is (andEL (Rlt x q) (Rlt q b00) Hqineq).
We prove the intermediate claim Hqltb00: Rlt q b00.
An exact proof term for the current goal is (andER (Rlt x q) (Rlt q b00) Hqineq).
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid 0 x q Hxle0 Hxltq).
We prove the intermediate claim HqS: SNo q.
An exact proof term for the current goal is (real_SNo q HqR).
We prove the intermediate claim Hqlt1: Rlt q 1.
Apply (SNoLt_trichotomy_or_impred 1 q SNo_1 HqS (Rlt q 1)) to the current goal.
Assume H1ltq: 1 < q.
Apply FalseE to the current goal.
We prove the intermediate claim H1ltb00: Rlt 1 b00.
An exact proof term for the current goal is (Rlt_tra 1 q b00 (RltI 1 q real_1 HqR H1ltq) Hqltb00).
An exact proof term for the current goal is ((andER (¬ (Rlt b00 0)) (¬ (Rlt 1 b00)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) b00 Hb00U)) H1ltb00).
Assume H1eq: 1 = q.
Apply FalseE to the current goal.
We prove the intermediate claim H1ltb00: Rlt 1 b00.
rewrite the current goal using H1eq (from left to right) at position 1.
An exact proof term for the current goal is Hqltb00.
An exact proof term for the current goal is ((andER (¬ (Rlt b00 0)) (¬ (Rlt 1 b00)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) b00 Hb00U)) H1ltb00).
Assume Hqlt1S: q < 1.
An exact proof term for the current goal is (RltI q 1 HqR real_1 Hqlt1S).
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.
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 (q,eps_ 1).
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 q (eps_ 1) HqU eps_1_in_unit_interval).
We prove the intermediate claim Hpw: order_rel (setprod R R) p w.
rewrite the current goal using HpEq (from left to right).
Apply (order_rel_setprod_R_R_intro x 1 q (eps_ 1)) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hxltq.
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 p w simply_ordered_set_setprod_R_R ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) a0 Ha0Sq) ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) p HpSq) ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) w HwSq) Ha0p Hpw).
We prove the intermediate claim Hwb0: order_rel (setprod R R) w b0.
Set b0eta to be the term (b00,b01).
We prove the intermediate claim Hb0Eta: b0 = b0eta.
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval b0 Hb0Sq).
rewrite the current goal using Hb0Eta (from left to right).
Apply (order_rel_setprod_R_R_intro q (eps_ 1) b00 b01) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hqltb00.
We prove the intermediate claim HwI: w ∈ I.
rewrite the current goal using HIeq (from left to right).
Apply (SepI ordered_square (λz : set ⇒ order_rel (setprod R R) a0 z ∧ order_rel (setprod R R) z 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 HwD: w ∈ ordsq_D.
Apply (SepI ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) w HwSq) to the current goal.
We use q to witness the existential quantifier.
We will prove w = (q,eps_ 1) ∧ Rlt 0 q ∧ Rlt q 1.
Apply andI to the current goal.
We will prove w = (q,eps_ 1) ∧ Rlt 0 q.
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 Hwcap: w ∈ U ∩ ordsq_D.
An exact proof term for the current goal is (binintersectI U ordsq_D w HwU HwD).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_D) w Hwcap).
Assume HIlow: I ∈ Blow.
We prove the intermediate claim Hexb: ∃b0 ∈ ordered_square, I = {z ∈ ordered_square|order_rel (setprod R R) z b0}.
An exact proof term for the current goal is (SepE2 (𝒫 ordered_square) (λJ0 : set ⇒ ∃b0 ∈ ordered_square, J0 = {z ∈ ordered_square|order_rel (setprod R R) z b0}) I HIlow).
Apply Hexb to the current goal.
Let b0 be given.
Assume Hb0pack.
Apply Hb0pack to the current goal.
Assume Hb0Sq HIeq.
We prove the intermediate claim HpI': p ∈ {z ∈ ordered_square|order_rel (setprod R R) z b0}.
rewrite the current goal using HIeq (from right to left).
An exact proof term for the current goal is HpI.
We prove the intermediate claim Hpb0: order_rel (setprod R R) p b0.
An exact proof term for the current goal is (SepE2 ordered_square (λz : set ⇒ order_rel (setprod R R) z b0) p HpI').
Set b00 to be the term b0 0.
Set b01 to be the term b0 1.
We prove the intermediate claim Hb00U: b00 ∈ unit_interval.
An exact proof term for the current goal is (ap0_Sigma unit_interval (λ_ : set ⇒ unit_interval) b0 Hb0Sq).
We prove the intermediate claim Hb01U: b01 ∈ unit_interval.
An exact proof term for the current goal is (ap1_Sigma unit_interval (λ_ : set ⇒ unit_interval) b0 Hb0Sq).
We prove the intermediate claim Hb00R: b00 ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R b00 Hb00U).
We prove the intermediate claim Hb00S: SNo b00.
An exact proof term for the current goal is (real_SNo b00 Hb00R).
We prove the intermediate claim Hb01not1: ¬ (Rlt 1 b01).
An exact proof term for the current goal is (andER (¬ (Rlt b01 0)) (¬ (Rlt 1 b01)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) b01 Hb01U)).
We prove the intermediate claim Hxltb00: Rlt x b00.
We prove the intermediate claim Hb0Eta: b0 = (b00,b01).
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval b0 Hb0Sq).
We prove the intermediate claim Hunf: ∃c1 c2 d1 d2 : set, p = (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 p b0 Hpb0).
Apply Hunf 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 Hcore2.
Apply Hcore2 to the current goal.
Assume Hab Hdisj.
Apply Hab to the current goal.
Assume HpEq2 HbEq2.
We prove the intermediate claim HpPair: (c1,c2) = (x,1).
We will prove (c1,c2) = (x,1).
rewrite the current goal using HpEq (from right to left).
rewrite the current goal using HpEq2 (from right to left).
Use reflexivity.
We prove the intermediate claim Hccoords: c1 = x ∧ c2 = 1.
An exact proof term for the current goal is (tuple_eq_coords c1 c2 x 1 HpPair).
We prove the intermediate claim Hc1eq: c1 = x.
An exact proof term for the current goal is (andEL (c1 = x) (c2 = 1) Hccoords).
We prove the intermediate claim Hc2eq: c2 = 1.
An exact proof term for the current goal is (andER (c1 = x) (c2 = 1) Hccoords).
We prove the intermediate claim HbPair: (d1,d2) = (b00,b01).
We will prove (d1,d2) = (b00,b01).
rewrite the current goal using Hb0Eta (from right to left).
rewrite the current goal using HbEq2 (from right to left).
Use reflexivity.
We prove the intermediate claim Hdcoords: d1 = b00 ∧ d2 = b01.
An exact proof term for the current goal is (tuple_eq_coords d1 d2 b00 b01 HbPair).
We prove the intermediate claim Hd1eq: d1 = b00.
An exact proof term for the current goal is (andEL (d1 = b00) (d2 = b01) Hdcoords).
We prove the intermediate claim Hd2eq: d2 = b01.
An exact proof term for the current goal is (andER (d1 = b00) (d2 = b01) Hdcoords).
Apply Hdisj 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).
An exact proof term for the current goal is Hlt.
Assume Heq: c1 = d1 ∧ Rlt c2 d2.
Apply FalseE to the current goal.
We prove the intermediate claim H1ltb01: Rlt 1 b01.
rewrite the current goal using Hc2eq (from right to left) at position 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).
An exact proof term for the current goal is (Hb01not1 H1ltb01).
Apply (rational_dense_between_reals x b00 HxR Hb00R Hxltb00) to the current goal.
Let q be given.
Assume Hqpack.
Apply Hqpack 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 Hxltq: Rlt x q.
An exact proof term for the current goal is (andEL (Rlt x q) (Rlt q b00) Hqineq).
We prove the intermediate claim Hqltb00: Rlt q b00.
An exact proof term for the current goal is (andER (Rlt x q) (Rlt q b00) Hqineq).
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid 0 x q Hxle0 Hxltq).
We prove the intermediate claim HqS: SNo q.
An exact proof term for the current goal is (real_SNo q HqR).
We prove the intermediate claim Hqlt1: Rlt q 1.
Apply (SNoLt_trichotomy_or_impred 1 q SNo_1 HqS (Rlt q 1)) to the current goal.
Assume H1ltq: 1 < q.
Apply FalseE to the current goal.
We prove the intermediate claim H1ltb00: Rlt 1 b00.
An exact proof term for the current goal is (Rlt_tra 1 q b00 (RltI 1 q real_1 HqR H1ltq) Hqltb00).
An exact proof term for the current goal is ((andER (¬ (Rlt b00 0)) (¬ (Rlt 1 b00)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) b00 Hb00U)) H1ltb00).
Assume H1eq: 1 = q.
Apply FalseE to the current goal.
We prove the intermediate claim H1ltb00: Rlt 1 b00.
rewrite the current goal using H1eq (from left to right) at position 1.
An exact proof term for the current goal is Hqltb00.
An exact proof term for the current goal is ((andER (¬ (Rlt b00 0)) (¬ (Rlt 1 b00)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) b00 Hb00U)) H1ltb00).
Assume Hqlt1S: q < 1.
An exact proof term for the current goal is (RltI q 1 HqR real_1 Hqlt1S).
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.
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 (q,eps_ 1).
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 q (eps_ 1) HqU eps_1_in_unit_interval).
We prove the intermediate claim Hwb0: order_rel (setprod R R) w b0.
We prove the intermediate claim Hb0Eta: b0 = (b00,b01).
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval b0 Hb0Sq).
rewrite the current goal using Hb0Eta (from left to right).
Apply (order_rel_setprod_R_R_intro q (eps_ 1) b00 b01) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hqltb00.
We prove the intermediate claim HwI: w ∈ I.
rewrite the current goal using HIeq (from left to right).
Apply (SepI ordered_square (λz : set ⇒ order_rel (setprod R R) z 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 HwD: w ∈ ordsq_D.
Apply (SepI ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) w HwSq) to the current goal.
We use q to witness the existential quantifier.
We will prove w = (q,eps_ 1) ∧ Rlt 0 q ∧ Rlt q 1.
Apply andI to the current goal.
We will prove w = (q,eps_ 1) ∧ Rlt 0 q.
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 Hwcap: w ∈ U ∩ ordsq_D.
An exact proof term for the current goal is (binintersectI U ordsq_D w HwU HwD).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_D) w Hwcap).
Assume HIup: I ∈ Bup.
We prove the intermediate claim Hexa: ∃a0 ∈ ordered_square, I = {z ∈ ordered_square|order_rel (setprod R R) a0 z}.
An exact proof term for the current goal is (SepE2 (𝒫 ordered_square) (λJ0 : set ⇒ ∃a0 ∈ ordered_square, J0 = {z ∈ ordered_square|order_rel (setprod R R) a0 z}) I HIup).
Apply Hexa to the current goal.
Let a0 be given.
Assume Ha0pack.
Apply Ha0pack to the current goal.
Assume Ha0Sq HIeq.
We prove the intermediate claim HpI': p ∈ {z ∈ ordered_square|order_rel (setprod R R) a0 z}.
rewrite the current goal using HIeq (from right to left).
An exact proof term for the current goal is HpI.
We prove the intermediate claim Ha0p: order_rel (setprod R R) a0 p.
An exact proof term for the current goal is (SepE2 ordered_square (λz : set ⇒ order_rel (setprod R R) a0 z) p HpI').
Apply (rational_dense_between_reals x 1 HxR real_1 Hxlt1) to the current goal.
Let q be given.
Assume Hqpack.
Apply Hqpack 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 Hxltq: Rlt x q.
An exact proof term for the current goal is (andEL (Rlt x q) (Rlt q 1) Hqineq).
We prove the intermediate claim Hqlt1: Rlt q 1.
An exact proof term for the current goal is (andER (Rlt x q) (Rlt q 1) Hqineq).
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid 0 x q Hxle0 Hxltq).
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.
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 (q,eps_ 1).
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 q (eps_ 1) HqU eps_1_in_unit_interval).
We prove the intermediate claim Hpw: order_rel (setprod R R) p w.
rewrite the current goal using HpEq (from left to right).
Apply (order_rel_setprod_R_R_intro x 1 q (eps_ 1)) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hxltq.
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 p w simply_ordered_set_setprod_R_R ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) a0 Ha0Sq) ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) p HpSq) ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) w HwSq) Ha0p Hpw).
We prove the intermediate claim HwI: w ∈ I.
rewrite the current goal using HIeq (from left to right).
Apply (SepI ordered_square (λz : set ⇒ order_rel (setprod R R) a0 z) 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 HwD: w ∈ ordsq_D.
Apply (SepI ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) w HwSq) to the current goal.
We use q to witness the existential quantifier.
We will prove w = (q,eps_ 1) ∧ Rlt 0 q ∧ Rlt q 1.
Apply andI to the current goal.
We will prove w = (q,eps_ 1) ∧ Rlt 0 q.
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 Hwcap: w ∈ U ∩ ordsq_D.
An exact proof term for the current goal is (binintersectI U ordsq_D w HwU HwD).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_D) w Hwcap).
∎