We will prove ordsq_p10 ∈ closure_of ordered_square ordered_square_topology ordsq_C.
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_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) 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_C ≠ 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.
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 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 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 Ha01R: a01 ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) a01 Ha01U).
We prove the intermediate claim Hb00R: b00 ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) b00 Hb00U).
We prove the intermediate claim Hb01R: b01 ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) b01 Hb01U).
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 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 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 Hunf1: ∃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).
We prove the intermediate claim Ha00lt1: Rlt a00 1.
Apply Hunf1 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 Hpair: a0 = (c1,c2) ∧ ordsq_p10 = (d1,d2).
An exact proof term for the current goal is (andEL (a0 = (c1,c2) ∧ ordsq_p10 = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim Ha0Eq: a0 = (c1,c2).
An exact proof term for the current goal is (andEL (a0 = (c1,c2)) (ordsq_p10 = (d1,d2)) Hpair).
We prove the intermediate claim Hp10Eq: ordsq_p10 = (d1,d2).
An exact proof term for the current goal is (andER (a0 = (c1,c2)) (ordsq_p10 = (d1,d2)) Hpair).
We prove the intermediate claim Hdisj: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).
An exact proof term for the current goal is (andER (a0 = (c1,c2) ∧ ordsq_p10 = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim Ha0coords: c1 = a00 ∧ c2 = a01.
We prove the intermediate claim Hc: (c1,c2) = (a00,a01).
rewrite the current goal using Ha0Eq (from right to left).
An exact proof term for the current goal is Ha0Eta.
An exact proof term for the current goal is (tuple_eq_coords c1 c2 a00 a01 Hc).
We prove the intermediate claim Hc1eq: c1 = a00.
An exact proof term for the current goal is (andEL (c1 = a00) (c2 = a01) Ha0coords).
We prove the intermediate claim Hc2eq: c2 = a01.
An exact proof term for the current goal is (andER (c1 = a00) (c2 = a01) Ha0coords).
We prove the intermediate claim Hp10def: ordsq_p10 = (1,0).
Use reflexivity.
We prove the intermediate claim Hp10coords: 1 = d1 ∧ 0 = d2.
We prove the intermediate claim Hpc: (1,0) = (d1,d2).
rewrite the current goal using Hp10def (from right to left).
An exact proof term for the current goal is Hp10Eq.
An exact proof term for the current goal is (tuple_eq_coords 1 0 d1 d2 Hpc).
We prove the intermediate claim Hd1eq: d1 = 1.
Use symmetry.
An exact proof term for the current goal is (andEL (1 = d1) (0 = d2) Hp10coords).
We prove the intermediate claim Hd2eq: d2 = 0.
Use symmetry.
An exact proof term for the current goal is (andER (1 = d1) (0 = d2) Hp10coords).
Apply Hdisj to the current goal.
Assume Hlt: Rlt c1 d1.
We will prove Rlt a00 1.
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 Hltc2d2: Rlt c2 d2.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Heq).
We prove the intermediate claim Ha01lt0: Rlt a01 0.
We will prove 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 Hltc2d2.
An exact proof term for the current goal is (Ha01notlt0 Ha01lt0).
We prove the intermediate claim Hunf2: ∃c1 c2 d1 d2 : set, ordsq_p10 = (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 ordsq_p10 b0 Hp10b0).
We prove the intermediate claim Hb00eq1: b00 = 1.
Apply Hunf2 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 Hpair: ordsq_p10 = (c1,c2) ∧ b0 = (d1,d2).
An exact proof term for the current goal is (andEL (ordsq_p10 = (c1,c2) ∧ b0 = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim Hp10Eq: ordsq_p10 = (c1,c2).
An exact proof term for the current goal is (andEL (ordsq_p10 = (c1,c2)) (b0 = (d1,d2)) Hpair).
We prove the intermediate claim Hb0Eq: b0 = (d1,d2).
An exact proof term for the current goal is (andER (ordsq_p10 = (c1,c2)) (b0 = (d1,d2)) Hpair).
We prove the intermediate claim Hdisj: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).
An exact proof term for the current goal is (andER (ordsq_p10 = (c1,c2) ∧ b0 = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim Hp10def: ordsq_p10 = (1,0).
Use reflexivity.
We prove the intermediate claim Hp10coords: 1 = c1 ∧ 0 = c2.
We prove the intermediate claim Hpc: (1,0) = (c1,c2).
rewrite the current goal using Hp10def (from right to left).
An exact proof term for the current goal is Hp10Eq.
An exact proof term for the current goal is (tuple_eq_coords 1 0 c1 c2 Hpc).
We prove the intermediate claim Hc1eq: c1 = 1.
Use symmetry.
An exact proof term for the current goal is (andEL (1 = c1) (0 = c2) Hp10coords).
We prove the intermediate claim Hb0coords: d1 = b00 ∧ d2 = b01.
We prove the intermediate claim Hd: (d1,d2) = (b00,b01).
rewrite the current goal using Hb0Eq (from right to left).
An exact proof term for the current goal is Hb0Eta.
An exact proof term for the current goal is (tuple_eq_coords d1 d2 b00 b01 Hd).
We prove the intermediate claim Hd1eq: d1 = b00.
An exact proof term for the current goal is (andEL (d1 = b00) (d2 = b01) Hb0coords).
Apply Hdisj to the current goal.
Assume Hlt: Rlt c1 d1.
Apply FalseE to the current goal.
We prove the intermediate claim H1ltb00: Rlt 1 b00.
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.
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 Heq: c1 = d1 ∧ Rlt c2 d2.
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 will prove b00 = 1.
rewrite the current goal using Hd1eq (from right to left).
rewrite the current goal using Hc1d1 (from right to left).
rewrite the current goal using Hc1eq (from left to right).
Use reflexivity.
We prove the intermediate claim Hqex: ∃q ∈ rational_numbers, Rlt a00 q ∧ Rlt q 1.
An exact proof term for the current goal is (rational_dense_between_reals a00 1 Ha00R real_1 Ha00lt1).
Apply Hqex to the current goal.
Let q be given.
Assume Hqpack.
Apply Hqpack to the current goal.
Assume HqQ Hqineq.
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 HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
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 Hnotq0: ¬ (Rlt q 0).
Assume Hqlt0: Rlt q 0.
We prove the intermediate claim Ha00lt0: Rlt a00 0.
An exact proof term for the current goal is (Rlt_tra a00 q 0 Ha00ltq Hqlt0).
An exact proof term for the current goal is (Ha00notlt0 Ha00lt0).
We prove the intermediate claim Hqneq0: ¬ (q = 0).
Assume Hq0: q = 0.
We prove the intermediate claim Ha00lt0: Rlt a00 0.
We will prove Rlt a00 0.
rewrite the current goal using Hq0 (from right to left) at position 2.
An exact proof term for the current goal is Ha00ltq.
An exact proof term for the current goal is (Ha00notlt0 Ha00lt0).
We prove the intermediate claim H0ltqS: 0 < q.
Apply (SNoLt_trichotomy_or_impred q 0 HqS SNo_0 (0 < q)) to the current goal.
Assume Hqlt0S: q < 0.
Apply FalseE to the current goal.
We prove the intermediate claim Hqlt0: Rlt q 0.
An exact proof term for the current goal is (RltI q 0 HqR real_0 Hqlt0S).
An exact proof term for the current goal is (Hnotq0 Hqlt0).
Assume Hqeq0S: q = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hqneq0 Hqeq0S).
Assume H0ltqS: 0 < q.
An exact proof term for the current goal is H0ltqS.
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (RltI 0 q real_0 HqR H0ltqS).
We prove the intermediate claim Hnot1q: ¬ (Rlt 1 q).
An exact proof term for the current goal is (not_Rlt_sym q 1 Hqlt1).
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 Hnotq0.
An exact proof term for the current goal is Hnot1q.
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 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 0) 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 0 b00 b01) to the current goal.
Apply orIL to the current goal.
rewrite the current goal using Hb00eq1 (from left to right).
An exact proof term for the current goal is Hqlt1.
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 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 Hwcap: 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 Hwcap).
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': ordsq_p10 ∈ {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 Hp10I.
We prove the intermediate claim Hp10b: order_rel (setprod R R) ordsq_p10 b.
An exact proof term for the current goal is (SepE2 ordered_square (λz : set ⇒ order_rel (setprod R R) z b) ordsq_p10 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 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 Hb0prop: ¬ (Rlt 1 (b 0)).
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)).
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 Hexunf: ∃c1 c2 d1 d2 : set, ordsq_p10 = (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 ordsq_p10 b Hp10b).
Apply Hexunf 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 Hpair: ordsq_p10 = (c1,c2) ∧ b = (d1,d2).
An exact proof term for the current goal is (andEL (ordsq_p10 = (c1,c2) ∧ b = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim Hp10Eq: ordsq_p10 = (c1,c2).
An exact proof term for the current goal is (andEL (ordsq_p10 = (c1,c2)) (b = (d1,d2)) Hpair).
We prove the intermediate claim HbEq: b = (d1,d2).
An exact proof term for the current goal is (andER (ordsq_p10 = (c1,c2)) (b = (d1,d2)) Hpair).
We prove the intermediate claim Hdisj: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).
An exact proof term for the current goal is (andER (ordsq_p10 = (c1,c2) ∧ b = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim Hp10def: ordsq_p10 = (1,0).
Use reflexivity.
We prove the intermediate claim Hp10coords: 1 = c1 ∧ 0 = c2.
We prove the intermediate claim Hpc: (1,0) = (c1,c2).
rewrite the current goal using Hp10def (from right to left).
An exact proof term for the current goal is Hp10Eq.
An exact proof term for the current goal is (tuple_eq_coords 1 0 c1 c2 Hpc).
We prove the intermediate claim Hc1eq: c1 = 1.
Use symmetry.
An exact proof term for the current goal is (andEL (1 = c1) (0 = c2) Hp10coords).
We prove the intermediate claim Hc2eq: c2 = 0.
Use symmetry.
An exact proof term for the current goal is (andER (1 = c1) (0 = c2) Hp10coords).
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 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 Hepsltb0: Rlt (eps_ 1) (b 0).
Apply Hdisj to the current goal.
Assume Hlt: Rlt c1 d1.
Apply FalseE to the current goal.
We prove the intermediate claim H1ltb0: Rlt 1 (b 0).
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.
An exact proof term for the current goal is (Hb0prop H1ltb0).
Assume Heq: c1 = d1 ∧ Rlt c2 d2.
We prove the intermediate claim Hc1d1: c1 = d1.
An exact proof term for the current goal is (andEL (c1 = d1) (Rlt c2 d2) Heq).
rewrite the current goal using Hd1eq (from right to left).
rewrite the current goal using Hc1d1 (from right to left).
rewrite the current goal using Hc1eq (from left to right).
An exact proof term for the current goal is eps_1_lt1_R.
Set w to be the term (eps_ 1,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 (eps_ 1) 0 eps_1_in_unit_interval 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 (eps_ 1) 0 (b 0) (b 1)) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hepsltb0.
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.
rewrite the current goal using HbEta (from left to right).
Apply (order_rel_setprod_R_R_intro (eps_ 1) 0 (b 0) (b 1)) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hepsltb0.
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 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 (eps_ 1) to witness the existential quantifier.
We will prove w = (eps_ 1,0) ∧ Rlt 0 (eps_ 1) ∧ Rlt (eps_ 1) 1.
Apply andI to the current goal.
We will prove w = (eps_ 1,0) ∧ 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 Hwcap: 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 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 ⇒ ∃a1 ∈ ordered_square, J0 = {z ∈ ordered_square|order_rel (setprod R R) a1 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': ordsq_p10 ∈ {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 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 (λz : set ⇒ order_rel (setprod R R) a0 z) ordsq_p10 HpI').
Set a00 to be the term a0 0.
Set a01 to be the term a0 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 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 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 Ha01R: a01 ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) a01 Ha01U).
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 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 Ha00S: SNo a00.
An exact proof term for the current goal is (real_SNo a00 Ha00R).
We prove the intermediate claim H1S: SNo 1.
An exact proof term for the current goal is (real_SNo 1 real_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).
We prove the intermediate claim Ha00lt1: Rlt a00 1.
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.
We prove the intermediate claim Hpair: a0 = (c1,c2) ∧ ordsq_p10 = (d1,d2).
An exact proof term for the current goal is (andEL (a0 = (c1,c2) ∧ ordsq_p10 = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim Ha0Eq: a0 = (c1,c2).
An exact proof term for the current goal is (andEL (a0 = (c1,c2)) (ordsq_p10 = (d1,d2)) Hpair).
We prove the intermediate claim Hp10Eq: ordsq_p10 = (d1,d2).
An exact proof term for the current goal is (andER (a0 = (c1,c2)) (ordsq_p10 = (d1,d2)) Hpair).
We prove the intermediate claim Hdisj: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).
An exact proof term for the current goal is (andER (a0 = (c1,c2) ∧ ordsq_p10 = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hcore).
We prove the intermediate claim Ha0coords: c1 = a00 ∧ c2 = a01.
We prove the intermediate claim Hc: (c1,c2) = (a00,a01).
rewrite the current goal using Ha0Eq (from right to left).
An exact proof term for the current goal is Ha0Eta.
An exact proof term for the current goal is (tuple_eq_coords c1 c2 a00 a01 Hc).
We prove the intermediate claim Hc1eq: c1 = a00.
An exact proof term for the current goal is (andEL (c1 = a00) (c2 = a01) Ha0coords).
We prove the intermediate claim Hc2eq: c2 = a01.
An exact proof term for the current goal is (andER (c1 = a00) (c2 = a01) Ha0coords).
We prove the intermediate claim Hp10def: ordsq_p10 = (1,0).
Use reflexivity.
We prove the intermediate claim Hp10coords: 1 = d1 ∧ 0 = d2.
We prove the intermediate claim Hpc: (1,0) = (d1,d2).
rewrite the current goal using Hp10def (from right to left).
An exact proof term for the current goal is Hp10Eq.
An exact proof term for the current goal is (tuple_eq_coords 1 0 d1 d2 Hpc).
We prove the intermediate claim Hd1eq: d1 = 1.
Use symmetry.
An exact proof term for the current goal is (andEL (1 = d1) (0 = d2) Hp10coords).
We prove the intermediate claim Hd2eq: d2 = 0.
Use symmetry.
An exact proof term for the current goal is (andER (1 = d1) (0 = d2) Hp10coords).
Apply Hdisj to the current goal.
Assume Hlt: Rlt c1 d1.
We will prove Rlt a00 1.
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 Hltc2d2: Rlt c2 d2.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Heq).
We prove the intermediate claim Ha01lt0: Rlt a01 0.
We will prove 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 Hltc2d2.
An exact proof term for the current goal is (Ha01notlt0 Ha01lt0).
We prove the intermediate claim Hqex: ∃q ∈ rational_numbers, Rlt a00 q ∧ Rlt q 1.
An exact proof term for the current goal is (rational_dense_between_reals a00 1 Ha00R real_1 Ha00lt1).
Apply Hqex to the current goal.
Let q be given.
Assume Hqpack.
Apply Hqpack to the current goal.
Assume HqQ Hqineq.
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 HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
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 Hnotq0: ¬ (Rlt q 0).
Assume Hqlt0: Rlt q 0.
We prove the intermediate claim Ha00lt0: Rlt a00 0.
An exact proof term for the current goal is (Rlt_tra a00 q 0 Ha00ltq Hqlt0).
An exact proof term for the current goal is (Ha00notlt0 Ha00lt0).
We prove the intermediate claim Hqneq0: ¬ (q = 0).
Assume Hq0: q = 0.
We prove the intermediate claim Ha00lt0: Rlt a00 0.
We will prove Rlt a00 0.
rewrite the current goal using Hq0 (from right to left) at position 2.
An exact proof term for the current goal is Ha00ltq.
An exact proof term for the current goal is (Ha00notlt0 Ha00lt0).
We prove the intermediate claim H0ltqS: 0 < q.
Apply (SNoLt_trichotomy_or_impred q 0 HqS SNo_0 (0 < q)) to the current goal.
Assume Hqlt0S: q < 0.
Apply FalseE to the current goal.
We prove the intermediate claim Hqlt0: Rlt q 0.
An exact proof term for the current goal is (RltI q 0 HqR real_0 Hqlt0S).
An exact proof term for the current goal is (Hnotq0 Hqlt0).
Assume Hqeq0S: q = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hqneq0 Hqeq0S).
Assume H0ltqS: 0 < q.
An exact proof term for the current goal is H0ltqS.
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (RltI 0 q real_0 HqR H0ltqS).
We prove the intermediate claim Hnot1q: ¬ (Rlt 1 q).
An exact proof term for the current goal is (not_Rlt_sym q 1 Hqlt1).
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 Hnotq0.
An exact proof term for the current goal is Hnot1q.
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 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 0) 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 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 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 Hwcap: 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 Hwcap).
∎