Let p be given.
Assume HpTop: p ∈ ordsq_top_edge_lt1.
We will prove p ∈ closure_of ordered_square ordered_square_topology 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 ⇒ ∃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 (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) 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 Hdefcl: closure_of ordered_square ordered_square_topology ordsq_C = {x0 ∈ ordered_square|∀U : set, U ∈ ordered_square_topology → x0 ∈ U → U ∩ ordsq_C ≠ 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_C ≠ 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_C ≠ 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: ∃a ∈ ordered_square, ∃b ∈ ordered_square, I = {z ∈ ordered_square|order_rel (setprod R R) a z ∧ order_rel (setprod R R) z b}.
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 a be given.
Assume Hapack.
Apply Hapack to the current goal.
Assume HaSq Hexb.
Apply Hexb to the current goal.
Let b be given.
Assume Hbpack.
Apply Hbpack to the current goal.
Assume HbSq HIeq.
We prove the intermediate claim HpI': p ∈ {z ∈ ordered_square|order_rel (setprod R R) a z ∧ order_rel (setprod R R) z b}.
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 Hpord: order_rel (setprod R R) a p ∧ order_rel (setprod R R) p b.
An exact proof term for the current goal is (SepE2 ordered_square (λz : set ⇒ order_rel (setprod R R) a z ∧ order_rel (setprod R R) z b) p HpI').
We prove the intermediate claim Hap: order_rel (setprod R R) a p.
An exact proof term for the current goal is (andEL (order_rel (setprod R R) a p) (order_rel (setprod R R) p b) Hpord).
We prove the intermediate claim Hpb: order_rel (setprod R R) p b.
An exact proof term for the current goal is (andER (order_rel (setprod R R) a p) (order_rel (setprod R R) p b) Hpord).
We prove the intermediate claim HbEta: b = (b 0,b 1).
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval b HbSq).
We prove the intermediate claim Hb0U: (b 0) ∈ unit_interval.
An exact proof term for the current goal is (ap0_Sigma unit_interval (λ_ : set ⇒ unit_interval) b HbSq).
We prove the intermediate claim Hb1U: (b 1) ∈ unit_interval.
An exact proof term for the current goal is (ap1_Sigma unit_interval (λ_ : set ⇒ unit_interval) b HbSq).
We prove the intermediate claim Hb0R: (b 0) ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (b 0) Hb0U).
We prove the intermediate claim Hb0S: SNo (b 0).
An exact proof term for the current goal is (real_SNo (b 0) Hb0R).
We prove the intermediate claim Hb1prop: ¬ (Rlt 1 (b 1)).
An exact proof term for the current goal is (andER (¬ (Rlt (b 1) 0)) (¬ (Rlt 1 (b 1))) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (b 1) Hb1U)).
We prove the intermediate claim Hxltb0: Rlt x (b 0).
We prove the intermediate claim Hpb_unf: ∃c1 c2 d1 d2 : set, p = (c1,c2) ∧ b = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).
An exact proof term for the current goal is (order_rel_setprod_R_R_unfold p b Hpb).
Apply Hpb_unf to the current goal.
Let c1 be given.
Assume Hc2.
Apply Hc2 to the current goal.
Let c2 be given.
Assume Hd1.
Apply Hd1 to the current goal.
Let d1 be given.
Assume Hd2.
Apply Hd2 to the current goal.
Let d2 be given.
Assume Hcore.
We prove the intermediate claim Hpb': p = (c1,c2) ∧ b = (d1,d2).
An exact proof term for the current goal is (andEL (p = (c1,c2) ∧ b = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim HpEq': p = (c1,c2).
An exact proof term for the current goal is (andEL (p = (c1,c2)) (b = (d1,d2)) Hpb').
We prove the intermediate claim HbEq': b = (d1,d2).
An exact proof term for the current goal is (andER (p = (c1,c2)) (b = (d1,d2)) Hpb').
We prove the intermediate claim Hdisj: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).
An exact proof term for the current goal is (andER (p = (c1,c2) ∧ b = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim Hpcoords: x = c1 ∧ 1 = c2.
We prove the intermediate claim Hpc: (x,1) = (c1,c2).
rewrite the current goal using HpEq (from right to left).
An exact proof term for the current goal is HpEq'.
An exact proof term for the current goal is (tuple_eq_coords x 1 c1 c2 Hpc).
We prove the intermediate claim Hc1eq: c1 = x.
Use symmetry.
An exact proof term for the current goal is (andEL (x = c1) (1 = c2) Hpcoords).
We prove the intermediate claim Hbcoords: d1 = (b 0) ∧ d2 = (b 1).
We prove the intermediate claim Hbd: (d1,d2) = (b 0,b 1).
rewrite the current goal using HbEq' (from right to left).
An exact proof term for the current goal is HbEta.
An exact proof term for the current goal is (tuple_eq_coords d1 d2 (b 0) (b 1) Hbd).
We prove the intermediate claim Hd1eq: d1 = (b 0).
An exact proof term for the current goal is (andEL (d1 = (b 0)) (d2 = (b 1)) Hbcoords).
We prove the intermediate claim Hcase: Rlt x (b 0) ∨ (x = (b 0) ∧ Rlt 1 (b 1)).
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.
We prove the intermediate claim Hc1d1: c1 = d1.
An exact proof term for the current goal is (andEL (c1 = d1) (Rlt c2 d2) Heq).
We prove the intermediate claim Hc2d2: Rlt c2 d2.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Heq).
Apply andI to the current goal.
We will prove x = (b 0).
rewrite the current goal using Hc1eq (from right to left).
rewrite the current goal using Hd1eq (from right to left).
An exact proof term for the current goal is Hc1d1.
We will prove Rlt 1 (b 1).
We prove the intermediate claim Hc2eq: c2 = 1.
Use symmetry.
An exact proof term for the current goal is (andER (x = c1) (1 = c2) Hpcoords).
We prove the intermediate claim Hd2eq: d2 = (b 1).
An exact proof term for the current goal is (andER (d1 = (b 0)) (d2 = (b 1)) Hbcoords).
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 Hc2d2.
Apply Hcase to the current goal.
Assume H1: Rlt x (b 0).
An exact proof term for the current goal is H1.
Assume H2: x = (b 0) ∧ Rlt 1 (b 1).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hb1prop (andER (x = (b 0)) (Rlt 1 (b 1)) H2)).
Apply (rational_dense_between_reals x (b 0) HxR Hb0R Hxltb0) 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 (b 0)) Hqineq).
We prove the intermediate claim Hqltb0: Rlt q (b 0).
An exact proof term for the current goal is (andER (Rlt x q) (Rlt q (b 0)) Hqineq).
We prove the intermediate claim HqU: q ∈ unit_interval.
Apply (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) q HqR) to the current goal.
Apply andI to the current goal.
We will prove ¬ (Rlt q 0).
Assume Hq0: Rlt q 0.
We prove the intermediate claim Hx0: Rlt x 0.
An exact proof term for the current goal is (Rlt_tra x q 0 Hxltq Hq0).
An exact proof term for the current goal is (Hxnotlt0 Hx0).
We will prove ¬ (Rlt 1 q).
Assume H1q: Rlt 1 q.
We prove the intermediate claim H1b0: Rlt 1 (b 0).
An exact proof term for the current goal is (Rlt_tra 1 q (b 0) H1q Hqltb0).
An exact proof term for the current goal is (andER (¬ (Rlt (b 0) 0)) (¬ (Rlt 1 (b 0))) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (b 0) Hb0U) H1b0).
Set w to be the term (q,0).
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 0 HqU zero_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 0) 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 Haw: order_rel (setprod R R) a w.
An exact proof term for the current goal is (order_rel_trans (setprod R R) a p w simply_ordered_set_setprod_R_R ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) a HaSq) ((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) Hap Hpw).
We prove the intermediate claim Hwb: order_rel (setprod R R) w b.
rewrite the current goal using HbEta (from left to right).
Apply (order_rel_setprod_R_R_intro q 0 (b 0) (b 1)) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hqltb0.
We prove the intermediate claim HwI: w ∈ I.
rewrite the current goal using HIeq (from left to right).
Apply (SepI ordered_square (λz : set ⇒ order_rel (setprod R R) a z ∧ order_rel (setprod R R) z b) w HwSq) to the current goal.
An exact proof term for the current goal is (andI (order_rel (setprod R R) a w) (order_rel (setprod R R) w b) Haw Hwb).
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 H0ltq: Rlt 0 q.
Apply (SNoLt_trichotomy_or_impred x 0 HxS SNo_0 (Rlt 0 q)) to the current goal.
Assume Hxlt0: x < 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnotlt0 (RltI x 0 HxR real_0 Hxlt0)).
Assume Hxeq0: x = 0.
rewrite the current goal using Hxeq0 (from right to left) at position 1.
An exact proof term for the current goal is Hxltq.
Assume H0ltx: 0 < x.
An exact proof term for the current goal is (Rlt_tra 0 x q (RltI 0 x real_0 HxR H0ltx) Hxltq).
We prove the intermediate claim Hqlt1: Rlt q 1.
Apply (SNoLt_trichotomy_or_impred (b 0) 1 Hb0S SNo_1 (Rlt q 1)) to the current goal.
Assume Hb0lt1: (b 0) < 1.
An exact proof term for the current goal is (Rlt_tra q (b 0) 1 Hqltb0 (RltI (b 0) 1 Hb0R real_1 Hb0lt1)).
Assume Hb0eq1: (b 0) = 1.
rewrite the current goal using Hb0eq1 (from right to left).
An exact proof term for the current goal is Hqltb0.
Assume H1ltb0: 1 < (b 0).
Apply FalseE to the current goal.
An exact proof term for the current goal is (andER (¬ (Rlt (b 0) 0)) (¬ (Rlt 1 (b 0))) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (b 0) Hb0U) (RltI 1 (b 0) real_1 Hb0R H1ltb0)).
We prove the intermediate claim HwC: w ∈ ordsq_C.
Apply (SepI ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,0) ∧ 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,0) ∧ Rlt 0 q ∧ Rlt q 1.
Apply andI to the current goal.
We will prove w = (q,0) ∧ 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 Hwc: w ∈ U ∩ ordsq_C.
An exact proof term for the current goal is (binintersectI U ordsq_C w HwU HwC).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_C) w Hwc).
Assume HIlow: I ∈ Blow.
We prove the intermediate claim Hexb: ∃b ∈ ordered_square, I = {z ∈ ordered_square|order_rel (setprod R R) z b}.
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 b be given.
Assume Hbpack.
Apply Hbpack to the current goal.
Assume HbSq HIeq.
We prove the intermediate claim HpI': p ∈ {z ∈ ordered_square|order_rel (setprod R R) z b}.
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 Hpb: order_rel (setprod R R) p b.
An exact proof term for the current goal is (SepE2 ordered_square (λz : set ⇒ order_rel (setprod R R) z b) p HpI').
We prove the intermediate claim HbEta: b = (b 0,b 1).
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval b HbSq).
We prove the intermediate claim Hb0U: (b 0) ∈ unit_interval.
An exact proof term for the current goal is (ap0_Sigma unit_interval (λ_ : set ⇒ unit_interval) b HbSq).
We prove the intermediate claim Hb0R: (b 0) ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (b 0) Hb0U).
We prove the intermediate claim Hb0S: SNo (b 0).
An exact proof term for the current goal is (real_SNo (b 0) Hb0R).
We prove the intermediate claim Hb1U: (b 1) ∈ unit_interval.
An exact proof term for the current goal is (ap1_Sigma unit_interval (λ_ : set ⇒ unit_interval) b HbSq).
We prove the intermediate claim Hb1prop: ¬ (Rlt 1 (b 1)).
An exact proof term for the current goal is (andER (¬ (Rlt (b 1) 0)) (¬ (Rlt 1 (b 1))) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (b 1) Hb1U)).
We prove the intermediate claim Hxltb0: Rlt x (b 0).
We prove the intermediate claim Hpb_unf: ∃c1 c2 d1 d2 : set, p = (c1,c2) ∧ b = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).
An exact proof term for the current goal is (order_rel_setprod_R_R_unfold p b Hpb).
Apply Hpb_unf to the current goal.
Let c1 be given.
Assume Hc2.
Apply Hc2 to the current goal.
Let c2 be given.
Assume Hd1.
Apply Hd1 to the current goal.
Let d1 be given.
Assume Hd2.
Apply Hd2 to the current goal.
Let d2 be given.
Assume Hcore.
We prove the intermediate claim Hpb': p = (c1,c2) ∧ b = (d1,d2).
An exact proof term for the current goal is (andEL (p = (c1,c2) ∧ b = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim HpEq': p = (c1,c2).
An exact proof term for the current goal is (andEL (p = (c1,c2)) (b = (d1,d2)) Hpb').
We prove the intermediate claim HbEq': b = (d1,d2).
An exact proof term for the current goal is (andER (p = (c1,c2)) (b = (d1,d2)) Hpb').
We prove the intermediate claim Hdisj: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).
An exact proof term for the current goal is (andER (p = (c1,c2) ∧ b = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim Hpcoords: x = c1 ∧ 1 = c2.
We prove the intermediate claim Hpc: (x,1) = (c1,c2).
rewrite the current goal using HpEq (from right to left).
An exact proof term for the current goal is HpEq'.
An exact proof term for the current goal is (tuple_eq_coords x 1 c1 c2 Hpc).
We prove the intermediate claim Hc1eq: c1 = x.
Use symmetry.
An exact proof term for the current goal is (andEL (x = c1) (1 = c2) Hpcoords).
We prove the intermediate claim Hbcoords: d1 = (b 0) ∧ d2 = (b 1).
We prove the intermediate claim Hbd: (d1,d2) = (b 0,b 1).
rewrite the current goal using HbEq' (from right to left).
An exact proof term for the current goal is HbEta.
An exact proof term for the current goal is (tuple_eq_coords d1 d2 (b 0) (b 1) Hbd).
We prove the intermediate claim Hd1eq: d1 = (b 0).
An exact proof term for the current goal is (andEL (d1 = (b 0)) (d2 = (b 1)) Hbcoords).
Apply Hdisj 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 Hc1d1: c1 = d1 ∧ Rlt c2 d2.
Apply FalseE to the current goal.
We prove the intermediate claim Hc2d2: Rlt c2 d2.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Hc1d1).
We prove the intermediate claim Hc2eq: c2 = 1.
Use symmetry.
An exact proof term for the current goal is (andER (x = c1) (1 = c2) Hpcoords).
We prove the intermediate claim Hd2eq: d2 = (b 1).
An exact proof term for the current goal is (andER (d1 = (b 0)) (d2 = (b 1)) Hbcoords).
We prove the intermediate claim H1ltb1: Rlt 1 (b 1).
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 Hc2d2.
An exact proof term for the current goal is (Hb1prop H1ltb1).
Apply (rational_dense_between_reals x (b 0) HxR Hb0R Hxltb0) 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 (b 0)) Hqineq).
We prove the intermediate claim Hqltb0: Rlt q (b 0).
An exact proof term for the current goal is (andER (Rlt x q) (Rlt q (b 0)) Hqineq).
We prove the intermediate claim HqU: q ∈ unit_interval.
Apply (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) q HqR) to the current goal.
Apply andI to the current goal.
We will prove ¬ (Rlt q 0).
Assume Hq0: Rlt q 0.
We prove the intermediate claim Hx0: Rlt x 0.
An exact proof term for the current goal is (Rlt_tra x q 0 Hxltq Hq0).
An exact proof term for the current goal is (Hxnotlt0 Hx0).
We will prove ¬ (Rlt 1 q).
Assume H1q: Rlt 1 q.
We prove the intermediate claim H1b0: Rlt 1 (b 0).
An exact proof term for the current goal is (Rlt_tra 1 q (b 0) H1q Hqltb0).
An exact proof term for the current goal is (andER (¬ (Rlt (b 0) 0)) (¬ (Rlt 1 (b 0))) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (b 0) Hb0U) H1b0).
Set w to be the term (q,0).
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 0 HqU zero_in_unit_interval).
We prove the intermediate claim Hwb: order_rel (setprod R R) w b.
rewrite the current goal using HbEta (from left to right).
Apply (order_rel_setprod_R_R_intro q 0 (b 0) (b 1)) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hqltb0.
We prove the intermediate claim 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 b) w HwSq) to the current goal.
An exact proof term for the current goal is Hwb.
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 H0ltq: Rlt 0 q.
Apply (SNoLt_trichotomy_or_impred x 0 HxS SNo_0 (Rlt 0 q)) to the current goal.
Assume Hxlt0: x < 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnotlt0 (RltI x 0 HxR real_0 Hxlt0)).
Assume Hxeq0: x = 0.
rewrite the current goal using Hxeq0 (from right to left) at position 1.
An exact proof term for the current goal is Hxltq.
Assume H0ltx: 0 < x.
An exact proof term for the current goal is (Rlt_tra 0 x q (RltI 0 x real_0 HxR H0ltx) Hxltq).
We prove the intermediate claim Hqlt1: Rlt q 1.
Apply (SNoLt_trichotomy_or_impred (b 0) 1 Hb0S SNo_1 (Rlt q 1)) to the current goal.
Assume Hb0lt1: (b 0) < 1.
An exact proof term for the current goal is (Rlt_tra q (b 0) 1 Hqltb0 (RltI (b 0) 1 Hb0R real_1 Hb0lt1)).
Assume Hb0eq1: (b 0) = 1.
rewrite the current goal using Hb0eq1 (from right to left).
An exact proof term for the current goal is Hqltb0.
Assume H1ltb0: 1 < (b 0).
Apply FalseE to the current goal.
An exact proof term for the current goal is (andER (¬ (Rlt (b 0) 0)) (¬ (Rlt 1 (b 0))) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (b 0) Hb0U) (RltI 1 (b 0) real_1 Hb0R H1ltb0)).
We prove the intermediate claim HwC: w ∈ ordsq_C.
Apply (SepI ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,0) ∧ 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,0) ∧ Rlt 0 q ∧ Rlt q 1.
Apply andI to the current goal.
We will prove w = (q,0) ∧ 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 Hwc: w ∈ U ∩ ordsq_C.
An exact proof term for the current goal is (binintersectI U ordsq_C w HwU HwC).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_C) w Hwc).
Assume HIup: I ∈ Bup.
We prove the intermediate claim Hexa: ∃a ∈ ordered_square, I = {z ∈ ordered_square|order_rel (setprod R R) a 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 a be given.
Assume Hapack.
Apply Hapack to the current goal.
Assume HaSq HIeq.
We prove the intermediate claim HpI': p ∈ {z ∈ ordered_square|order_rel (setprod R R) a 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 Hap: order_rel (setprod R R) a p.
An exact proof term for the current goal is (SepE2 ordered_square (λz : set ⇒ order_rel (setprod R R) a 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 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 Hx0: Rlt x 0.
An exact proof term for the current goal is (Rlt_tra x q 0 Hxltq Hq0).
An exact proof term for the current goal is (Hxnotlt0 Hx0).
We will prove ¬ (Rlt 1 q).
Assume H1q: Rlt 1 q.
An exact proof term for the current goal is ((not_Rlt_sym q 1 Hqlt1) H1q).
Set w to be the term (q,0).
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 0 HqU zero_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 0) 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 Haw: order_rel (setprod R R) a w.
An exact proof term for the current goal is (order_rel_trans (setprod R R) a p w simply_ordered_set_setprod_R_R ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) a HaSq) ((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) Hap 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) a z) w HwSq) to the current goal.
An exact proof term for the current goal is Haw.
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 H0ltq: Rlt 0 q.
Apply (SNoLt_trichotomy_or_impred x 0 HxS SNo_0 (Rlt 0 q)) to the current goal.
Assume Hxlt0: x < 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnotlt0 (RltI x 0 HxR real_0 Hxlt0)).
Assume Hxeq0: x = 0.
rewrite the current goal using Hxeq0 (from right to left) at position 1.
An exact proof term for the current goal is Hxltq.
Assume H0ltx: 0 < x.
An exact proof term for the current goal is (Rlt_tra 0 x q (RltI 0 x real_0 HxR H0ltx) Hxltq).
We prove the intermediate claim HwC: w ∈ ordsq_C.
Apply (SepI ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,0) ∧ 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,0) ∧ Rlt 0 q ∧ Rlt q 1.
Apply andI to the current goal.
We will prove w = (q,0) ∧ 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 Hwc: w ∈ U ∩ ordsq_C.
An exact proof term for the current goal is (binintersectI U ordsq_C w HwU HwC).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_C) w Hwc).
∎