Let p be given.
Assume HpC: p ∈ ordsq_C.
We prove the intermediate claim HpSq: p ∈ ordered_square.
An exact proof term for the current goal is (SepE1 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,0) ∧ Rlt 0 x0 ∧ Rlt x0 1) p HpC).
We prove the intermediate claim Hexx: ∃x : set, p = (x,0) ∧ Rlt 0 x ∧ Rlt x 1.
An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,0) ∧ Rlt 0 x0 ∧ Rlt x0 1) p HpC).
Apply Hexx to the current goal.
Let x be given.
Assume Hxpack.
Apply Hxpack to the current goal.
Assume Hcore Hxlt1.
Apply Hcore to the current goal.
Assume Hpx Hxpos.
We prove the intermediate claim Hp0U: p 0 ∈ 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 Hp0eq: p 0 = x.
rewrite the current goal using Hpx (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_0_eq x 0).
We prove the intermediate claim HxU: x ∈ unit_interval.
rewrite the current goal using Hp0eq (from right to left) at position 1.
An exact proof term for the current goal is Hp0U.
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 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 a00 to be the term a0 0.
Set a01 to be the term a0 1.
Set b00 to be the term b0 0.
Set b01 to be the term b0 1.
We prove the intermediate claim Ha0Eta: a0 = (a00,a01).
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval a0 Ha0Sq).
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 Ha00U: a00 ∈ unit_interval.
An exact proof term for the current goal is (ap0_Sigma unit_interval (λ_ : set ⇒ unit_interval) a0 Ha0Sq).
We prove the intermediate claim Ha01U: a01 ∈ unit_interval.
An exact proof term for the current goal is (ap1_Sigma unit_interval (λ_ : set ⇒ unit_interval) a0 Ha0Sq).
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 Ha00R: a00 ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R a00 Ha00U).
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 Ha00S: SNo a00.
An exact proof term for the current goal is (real_SNo a00 Ha00R).
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 Ha01notlt0: ¬ (Rlt a01 0).
An exact proof term for the current goal is (andEL (¬ (Rlt a01 0)) (¬ (Rlt 1 a01)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) a01 Ha01U)).
We prove the intermediate claim Ha00ltx: Rlt a00 x.
We prove the intermediate claim Hunf: ∃c1 c2 d1 d2 : set, a0 = (c1,c2) ∧ p = (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 p Ha0p).
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 Ha0Eq HpEq.
We prove the intermediate claim HpPair: (d1,d2) = (x,0).
rewrite the current goal using Hpx (from right to left) at position 1.
rewrite the current goal using HpEq (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hd1eq: d1 = x.
We will prove d1 = x.
rewrite the current goal using (tuple_2_0_eq d1 d2) (from right to left) at position 1.
rewrite the current goal using HpPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_0_eq x 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 HpPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq x 0).
We prove the intermediate claim HcPair: (c1,c2) = (a00,a01).
rewrite the current goal using Ha0Eta (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 Hc1eq: c1 = a00.
We will prove c1 = a00.
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 a00 a01).
We prove the intermediate claim Hc2eq: c2 = a01.
We will prove c2 = a01.
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 a00 a01).
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 Ha01lt0: Rlt a01 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 (Ha01notlt0 Ha01lt0).
Apply (rational_dense_between_reals a00 x Ha00R HxR Ha00ltx) 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 Ha00ltq: Rlt a00 q.
An exact proof term for the current goal is (andEL (Rlt a00 q) (Rlt q x) Hqineq).
We prove the intermediate claim Hqltx: Rlt q x.
An exact proof term for the current goal is (andER (Rlt a00 q) (Rlt q x) Hqineq).
We prove the intermediate claim Hxlb00: Rlt x b00 ∨ (x = b00 ∧ Rlt 0 b01).
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 HpEq HbEq.
We prove the intermediate claim HpPair: (c1,c2) = (x,0).
rewrite the current goal using Hpx (from right to left) at position 1.
rewrite the current goal using HpEq (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hc1eq: c1 = x.
We will prove c1 = x.
rewrite the current goal using (tuple_2_0_eq c1 c2) (from right to left) at position 1.
rewrite the current goal using HpPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_0_eq x 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 HpPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq x 0).
We prove the intermediate claim HbPair: (d1,d2) = (b00,b01).
rewrite the current goal using Hb0Eta (from right to left) at position 1.
rewrite the current goal using HbEq (from right to left) at position 1.
Use reflexivity.
We prove the intermediate claim Hd1eq: d1 = b00.
We will prove d1 = b00.
rewrite the current goal using (tuple_2_0_eq d1 d2) (from right to left) at position 1.
rewrite the current goal using HbPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_0_eq b00 b01).
We prove the intermediate claim Hd2eq: d2 = b01.
We will prove d2 = b01.
rewrite the current goal using (tuple_2_1_eq d1 d2) (from right to left) at position 1.
rewrite the current goal using HbPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq b00 b01).
Apply Hdisj to the current goal.
Assume Hlt: Rlt c1 d1.
Apply orIL to the current goal.
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 orIR to the current goal.
Apply andI to the current goal.
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 (andEL (c1 = d1) (Rlt c2 d2) Heq).
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).
We prove the intermediate claim Hqltb00: Rlt q b00.
Apply (Hxlb00 (Rlt q b00)) to the current goal.
Assume Hxltb00: Rlt x b00.
An exact proof term for the current goal is (Rlt_tra q x b00 Hqltx Hxltb00).
Assume HxEq: x = b00 ∧ Rlt 0 b01.
rewrite the current goal using (andEL (x = b00) (Rlt 0 b01) HxEq) (from right to left).
An exact proof term for the current goal is Hqltx.
We prove the intermediate claim HqU: q ∈ unit_interval.
Apply (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) q HqR) to the current goal.
Apply andI to the current goal.
We will prove ¬ (Rlt q 0).
Assume Hq0: Rlt q 0.
We prove the intermediate claim Ha000: Rlt a00 0.
An exact proof term for the current goal is (Rlt_tra a00 q 0 Ha00ltq Hq0).
We prove the intermediate claim Ha00prop: ¬ (Rlt a00 0).
An exact proof term for the current goal is (andEL (¬ (Rlt a00 0)) (¬ (Rlt 1 a00)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) a00 Ha00U)).
An exact proof term for the current goal is (Ha00prop Ha000).
We will prove ¬ (Rlt 1 q).
Assume H1q: Rlt 1 q.
We prove the intermediate claim H1x: Rlt 1 x.
An exact proof term for the current goal is (Rlt_tra 1 q x H1q Hqltx).
We prove the intermediate claim Hnot1x: ¬ (Rlt 1 x).
An exact proof term for the current goal is (not_Rlt_sym x 1 Hxlt1).
An exact proof term for the current goal is (Hnot1x H1x).
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 Ha0w: order_rel (setprod R R) a0 w.
rewrite the current goal using Ha0Eta (from left to right).
Apply (order_rel_setprod_R_R_intro a00 a01 q (eps_ 1)) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Ha00ltq.
We prove the intermediate claim Hwb0: order_rel (setprod R R) w b0.
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 Hqlt1: Rlt q 1.
An exact proof term for the current goal is (Rlt_tra q x 1 Hqltx Hxlt1).
We prove the intermediate claim Ha00notlt0: ¬ (Rlt a00 0).
An exact proof term for the current goal is (andEL (¬ (Rlt a00 0)) (¬ (Rlt 1 a00)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) a00 Ha00U)).
We prove the intermediate claim Ha00le0: Rle 0 a00.
An exact proof term for the current goal is (RleI 0 a00 real_0 Ha00R Ha00notlt0).
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid 0 a00 q Ha00le0 Ha00ltq).
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').
Apply (rational_dense_between_reals 0 x real_0 HxR Hxpos) 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 H0ltq: Rlt 0 q.
An exact proof term for the current goal is (andEL (Rlt 0 q) (Rlt q x) Hqineq).
We prove the intermediate claim Hqltx: Rlt q x.
An exact proof term for the current goal is (andER (Rlt 0 q) (Rlt q x) Hqineq).
We prove the intermediate claim HqU: q ∈ unit_interval.
Apply (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) q HqR) to the current goal.
Apply andI to the current goal.
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 (Rlt_tra q x 1 Hqltx Hxlt1)).
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 Hwp: order_rel (setprod R R) w p.
rewrite the current goal using Hpx (from left to right).
Apply (order_rel_setprod_R_R_intro q (eps_ 1) x 0) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hqltx.
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 p b0 simply_ordered_set_setprod_R_R ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) w HwSq) ((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) b0 Hb0Sq) Hwp Hpb0).
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 Hqlt1: Rlt q 1.
An exact proof term for the current goal is (Rlt_tra q x 1 Hqltx Hxlt1).
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').
Set w to be the term (x,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 x (eps_ 1) HxU eps_1_in_unit_interval).
We prove the intermediate claim Hpw: order_rel (setprod R R) p w.
rewrite the current goal using Hpx (from left to right) at position 1.
Apply (order_rel_setprod_R_R_intro x 0 x (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 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 x to witness the existential quantifier.
We will prove w = (x,eps_ 1) ∧ Rlt 0 x ∧ Rlt x 1.
Apply andI to the current goal.
We will prove w = (x,eps_ 1) ∧ Rlt 0 x.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is Hxpos.
An exact proof term for the current goal is Hxlt1.
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).
∎