We will prove ordsq_p10 ∈ closure_of ordered_square ordered_square_topology ordsq_D.
We prove the intermediate claim Hp10Sq: ordsq_p10 ∈ ordered_square.
We prove the intermediate claim Hp10def: ordsq_p10 = (1,0).
Use reflexivity.
rewrite the current goal using Hp10def (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval 1 0 one_in_unit_interval zero_in_unit_interval).
We prove the intermediate claim 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) ordsq_p10 Hp10Sq) to the current goal.
Let U be given.
Assume HUtop: U ∈ ordered_square_topology.
Assume Hp10U: ordsq_p10 ∈ U.
We will prove U ∩ ordsq_D ≠ Empty.
We prove the intermediate claim HexI: ∃I ∈ ordered_square_order_basis, ordsq_p10 ∈ I ∧ I ⊆ U.
An exact proof term for the current goal is (generated_topology_local_refine ordered_square ordered_square_order_basis U ordsq_p10 HUtop Hp10U).
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 Hp10I 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': ordsq_p10 ∈ {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 Hp10I.
We prove the intermediate claim Hp10core: order_rel (setprod R R) a0 ordsq_p10 ∧ order_rel (setprod R R) ordsq_p10 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) ordsq_p10 HpI').
We prove the intermediate claim Ha0p10: order_rel (setprod R R) a0 ordsq_p10.
An exact proof term for the current goal is (andEL (order_rel (setprod R R) a0 ordsq_p10) (order_rel (setprod R R) ordsq_p10 b0) Hp10core).
We prove the intermediate claim Hp10b0: order_rel (setprod R R) ordsq_p10 b0.
An exact proof term for the current goal is (andER (order_rel (setprod R R) a0 ordsq_p10) (order_rel (setprod R R) ordsq_p10 b0) Hp10core).
Set a00 to be the term a0 0.
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 Ha00R: a00 ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) a00 Ha00U).
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 Ha0lt1: Rlt a00 1.
We prove the intermediate claim Hunf: ∃c1 c2 d1 d2 : set, a0 = (c1,c2) ∧ ordsq_p10 = (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 ordsq_p10 Ha0p10).
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 Hcore.
Apply Hcore to the current goal.
Assume Hab Hdisj.
Apply Hab to the current goal.
Assume Ha0Eta Hp10Eta.
We prove the intermediate claim Hp10def: ordsq_p10 = (1,0).
Use reflexivity.
We prove the intermediate claim HdPair: (d1,d2) = (1,0).
rewrite the current goal using Hp10def (from right to left) at position 1.
rewrite the current goal using Hp10Eta (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hd1eq: d1 = 1.
We will prove d1 = 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 1 0).
We prove the intermediate claim HcPair: (c1,c2) = (a0 0,a0 1).
rewrite the current goal using Ha0Eta (from right to left) at position 1.
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval a0 Ha0Sq).
We prove the intermediate claim Hc1eq: c1 = (a0 0).
We will prove c1 = (a0 0).
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 (a0 0) (a0 1)).
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) at position 1.
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 Hc2lt: Rlt c2 d2.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Heq).
We prove the intermediate claim Ha01U: (a0 1) ∈ 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 Ha01notlt0: ¬ (Rlt (a0 1) 0).
An exact proof term for the current goal is (andEL (¬ (Rlt (a0 1) 0)) (¬ (Rlt 1 (a0 1))) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (a0 1) Ha01U)).
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 HcPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq (a0 0) (a0 1)).
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 1 0).
We prove the intermediate claim Hbad: Rlt (a0 1) 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 Hc2lt.
An exact proof term for the current goal is (Ha01notlt0 Hbad).
Apply (rational_dense_between_reals a00 1 Ha00R real_1 Ha0lt1) 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 1) Hqineq).
We prove the intermediate claim Hqlt1: Rlt q 1.
An exact proof term for the current goal is (andER (Rlt a00 q) (Rlt q 1) Hqineq).
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 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 Ha0w: order_rel (setprod R R) a0 w.
We prove the intermediate claim Ha0Eta: a0 = (a0 0,a0 1).
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval a0 Ha0Sq).
rewrite the current goal using Ha0Eta (from left to right).
Apply (order_rel_setprod_R_R_intro (a0 0) (a0 1) 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 Hwp10: order_rel (setprod R R) w ordsq_p10.
We prove the intermediate claim Hp10def: ordsq_p10 = (1,0).
Use reflexivity.
rewrite the current goal using Hp10def (from left to right).
Apply (order_rel_setprod_R_R_intro q (eps_ 1) 1 0) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hqlt1.
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 ordsq_p10 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) ordsq_p10 Hp10Sq) ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) b0 Hb0Sq) Hwp10 Hp10b0).
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 Hwd: 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 Hwd).
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': ordsq_p10 ∈ {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 Hp10I.
We prove the intermediate claim Hp10b0: order_rel (setprod R R) ordsq_p10 b0.
An exact proof term for the current goal is (SepE2 ordered_square (λz : set ⇒ order_rel (setprod R R) z b0) ordsq_p10 HpI').
Set w to be the term (eps_ 1,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 (eps_ 1) (eps_ 1) eps_1_in_unit_interval eps_1_in_unit_interval).
We prove the intermediate claim Hwp10: order_rel (setprod R R) w ordsq_p10.
We prove the intermediate claim Hp10def: ordsq_p10 = (1,0).
Use reflexivity.
rewrite the current goal using Hp10def (from left to right).
Apply (order_rel_setprod_R_R_intro (eps_ 1) (eps_ 1) 1 0) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is eps_1_lt1_R.
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 ordsq_p10 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) ordsq_p10 Hp10Sq) ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) b0 Hb0Sq) Hwp10 Hp10b0).
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 (eps_ 1) to witness the existential quantifier.
We will prove w = (eps_ 1,eps_ 1) ∧ Rlt 0 (eps_ 1) ∧ Rlt (eps_ 1) 1.
Apply andI to the current goal.
We will prove w = (eps_ 1,eps_ 1) ∧ Rlt 0 (eps_ 1).
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is eps_1_pos_R.
An exact proof term for the current goal is eps_1_lt1_R.
We prove the intermediate claim Hwd: 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 Hwd).
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 HpI': ordsq_p10 ∈ {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 Hp10I.
We prove the intermediate claim Ha0p10: order_rel (setprod R R) a0 ordsq_p10.
An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0) ordsq_p10 HpI').
Set a00 to be the term a0 0.
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 Ha00R: a00 ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) a00 Ha00U).
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 Ha0lt1: Rlt a00 1.
We prove the intermediate claim Hunf: ∃c1 c2 d1 d2 : set, a0 = (c1,c2) ∧ ordsq_p10 = (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 ordsq_p10 Ha0p10).
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 Hcore.
Apply Hcore to the current goal.
Assume Hab Hdisj.
Apply Hab to the current goal.
Assume Ha0Eta Hp10Eta.
We prove the intermediate claim Hp10def: ordsq_p10 = (1,0).
Use reflexivity.
We prove the intermediate claim HdPair: (d1,d2) = (1,0).
rewrite the current goal using Hp10def (from right to left) at position 1.
rewrite the current goal using Hp10Eta (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hd1eq: d1 = 1.
We will prove d1 = 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 1 0).
We prove the intermediate claim HcPair: (c1,c2) = (a0 0,a0 1).
rewrite the current goal using Ha0Eta (from right to left) at position 1.
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval a0 Ha0Sq).
We prove the intermediate claim Hc1eq: c1 = (a0 0).
We will prove c1 = (a0 0).
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 (a0 0) (a0 1)).
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) at position 1.
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 Hc2lt: Rlt c2 d2.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Heq).
We prove the intermediate claim Ha01U: (a0 1) ∈ 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 Ha01notlt0: ¬ (Rlt (a0 1) 0).
An exact proof term for the current goal is (andEL (¬ (Rlt (a0 1) 0)) (¬ (Rlt 1 (a0 1))) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (a0 1) Ha01U)).
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 HcPair (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq (a0 0) (a0 1)).
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 1 0).
We prove the intermediate claim Hbad: Rlt (a0 1) 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 Hc2lt.
An exact proof term for the current goal is (Ha01notlt0 Hbad).
Apply (rational_dense_between_reals a00 1 Ha00R real_1 Ha0lt1) 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 1) Hqineq).
We prove the intermediate claim Hqlt1: Rlt q 1.
An exact proof term for the current goal is (andER (Rlt a00 q) (Rlt q 1) Hqineq).
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 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 Ha0w: order_rel (setprod R R) a0 w.
We prove the intermediate claim Ha0Eta: a0 = (a0 0,a0 1).
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval a0 Ha0Sq).
rewrite the current goal using Ha0Eta (from left to right).
Apply (order_rel_setprod_R_R_intro (a0 0) (a0 1) 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 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 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 Hwd: 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 Hwd).
∎