We prove the intermediate claim HpEq: p = ordsq_p01.

An exact proof term for the current goal is (SingE ordsq_p01 p Hp01).

rewrite the current goal using HpEq (from left to right).

Set p01 to be the term ordsq_p01.

We prove the intermediate claim Hp01def: p01 = (0,1).

Use reflexivity.

We prove the intermediate claim Hp01Sq: p01 ∈ ordered_square.

rewrite the current goal using Hp01def (from left to right).

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval 0 1 zero_in_unit_interval one_in_unit_interval).

We prove the intermediate claim Hdefcl: closure_of ordered_square ordered_square_topology ordsq_A = {x ∈ ordered_square|∀U : set, U ∈ ordered_square_topology → x ∈ U → U ∩ ordsq_A ≠ 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_A ≠ Empty) p01 Hp01Sq) to the current goal.

Let U be given.

Assume HUtop: U ∈ ordered_square_topology.

Assume Hp01U: p01 ∈ U.

We will prove U ∩ ordsq_A ≠ Empty.

We prove the intermediate claim HUgt: U ∈ generated_topology ordered_square ordered_square_order_basis.

We prove the intermediate claim HdefT: ordered_square_topology = generated_topology ordered_square ordered_square_order_basis.

Use reflexivity.

rewrite the current goal using HdefT (from right to left).

An exact proof term for the current goal is HUtop.

We prove the intermediate claim HexI: ∃I ∈ ordered_square_order_basis, p01 ∈ I ∧ I ⊆ U.

An exact proof term for the current goal is (generated_topology_local_refine ordered_square ordered_square_order_basis U p01 HUgt Hp01U).

Apply HexI to the current goal.

Let I be given.

Assume HIprop.

Apply HIprop to the current goal.

Assume HIbas HIcore.

Apply HIcore to the current goal.

Assume Hp01I HIU.

Set Bint to be the term {J ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, J = {x ∈ ordered_square|order_rel (setprod R R) a0 x ∧ order_rel (setprod R R) x b0}}.

Set Blow to be the term {J ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, J = {x ∈ ordered_square|order_rel (setprod R R) x b0}}.

Set Bup to be the term {J ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, J = {x ∈ ordered_square|order_rel (setprod R R) a0 x}}.

We prove the intermediate claim HIcase: I ∈ ((Bint ∪ Blow) ∪ Bup).

We prove the intermediate claim HdefB: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).

Use reflexivity.

rewrite the current goal using HdefB (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 HIint_ex: ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) a0 x ∧ order_rel (setprod R R) x b0}.

An exact proof term for the current goal is (SepE2 (𝒫 ordered_square) (λJ0 : set ⇒ ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, J0 = {x ∈ ordered_square|order_rel (setprod R R) a0 x ∧ order_rel (setprod R R) x b0}) I HIint).

Apply HIint_ex to the current goal.

Let a0 be given.

Assume Ha0rest.

Apply Ha0rest to the current goal.

Assume Ha0Sq Hb0core.

Apply Hb0core to the current goal.

Let b0 be given.

Assume Hb0rest.

Apply Hb0rest to the current goal.

Assume Hb0Sq HeqI.

We prove the intermediate claim Hp01I2: p01 ∈ {x ∈ ordered_square|order_rel (setprod R R) a0 x ∧ order_rel (setprod R R) x b0}.

rewrite the current goal using HeqI (from right to left).

An exact proof term for the current goal is Hp01I.

We prove the intermediate claim Hp01props: order_rel (setprod R R) a0 p01 ∧ order_rel (setprod R R) p01 b0.

An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0) p01 Hp01I2).

Apply Hp01props to the current goal.

Assume Ha0p01 Hp01b0.

We prove the intermediate claim Hb0xU: b0 0 ∈ 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 Hb0xR: b0 0 ∈ R.

An exact proof term for the current goal is (unit_interval_sub_R (b0 0) Hb0xU).

We prove the intermediate claim Hp01case: ∃c1 c2 d1 d2 : set, p01 = (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 p01 b0 Hp01b0).

Apply Hp01case 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 Hp01Eq Hb0Eq.

We prove the intermediate claim Hp01pair: (c1,c2) = (0,1).

rewrite the current goal using Hp01def (from right to left) at position 1.

rewrite the current goal using Hp01Eq (from left to right) at position 1.

Use reflexivity.

We prove the intermediate claim Hc1eq: c1 = 0.

We will prove c1 = 0.

rewrite the current goal using (tuple_2_0_eq c1 c2) (from right to left) at position 1.

rewrite the current goal using Hp01pair (from left to right) at position 1.

An exact proof term for the current goal is (tuple_2_0_eq 0 1).

We prove the intermediate claim Hc2eq: c2 = 1.

We will prove c2 = 1.

rewrite the current goal using (tuple_2_1_eq c1 c2) (from right to left) at position 1.

rewrite the current goal using Hp01pair (from left to right) at position 1.

An exact proof term for the current goal is (tuple_2_1_eq 0 1).

We prove the intermediate claim Hd1eq: d1 = (b0 0).

We will prove d1 = (b0 0).

rewrite the current goal using (tuple_2_0_eq d1 d2) (from right to left) at position 1.

rewrite the current goal using Hb0Eq (from right to left) at position 1.

Use reflexivity.

Apply Hdisj to the current goal.

Assume H0ltd1: Rlt c1 d1.

We prove the intermediate claim Hb0pos: Rlt 0 (b0 0).

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 H0ltd1.

Apply (exists_inv_nat_ordsucc_lt_local (b0 0) Hb0xR Hb0pos) to the current goal.

Let N be given.

Assume HNpack.

Apply HNpack to the current goal.

Assume HNO Hinvlt.

Set n0 to be the term ordsucc N.

We prove the intermediate claim Hn0O: n0 ∈ ω.

An exact proof term for the current goal is (omega_ordsucc N HNO).

We prove the intermediate claim Hn0not0: n0 ∉ {0}.

Assume Hn0in0: n0 ∈ {0}.

We prove the intermediate claim Hn0eq0: n0 = 0.

An exact proof term for the current goal is (SingE 0 n0 Hn0in0).

Apply FalseE to the current goal.

An exact proof term for the current goal is ((neq_ordsucc_0 N) Hn0eq0).

We prove the intermediate claim Hn0In: n0 ∈ ω ∖ {0}.

An exact proof term for the current goal is (setminusI ω {0} n0 Hn0O Hn0not0).

Set w to be the term (inv_nat n0,0).

We prove the intermediate claim HwA: w ∈ ordsq_A.

An exact proof term for the current goal is (ReplI (ω ∖ {0}) (λn1 : set ⇒ (inv_nat n1,0)) n0 Hn0In).

We prove the intermediate claim Hw0U: inv_nat n0 ∈ unit_interval.

We prove the intermediate claim HinvR: inv_nat n0 ∈ R.

An exact proof term for the current goal is (inv_nat_real n0 Hn0O).

We prove the intermediate claim Hinvpos: Rlt 0 (inv_nat n0).

An exact proof term for the current goal is (inv_nat_pos n0 Hn0In).

We prove the intermediate claim Hnlt0: ¬ (Rlt (inv_nat n0) 0).

An exact proof term for the current goal is (not_Rlt_sym 0 (inv_nat n0) Hinvpos).

We prove the intermediate claim Hinvle1: Rle (inv_nat n0) 1.

An exact proof term for the current goal is (inv_nat_Rle_1_local n0 Hn0In).

We prove the intermediate claim Hnlt1: ¬ (Rlt 1 (inv_nat n0)).

An exact proof term for the current goal is (RleE_nlt (inv_nat n0) 1 Hinvle1).

Apply (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (inv_nat n0) HinvR) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is Hnlt0.

An exact proof term for the current goal is Hnlt1.

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 (inv_nat n0) 0 Hw0U zero_in_unit_interval).

We prove the intermediate claim Hwltb0: order_rel (setprod R R) w b0.

rewrite the current goal using Hb0Eq (from left to right).

Apply (order_rel_setprod_R_R_intro (inv_nat n0) 0 d1 d2) to the current goal.

Apply orIL to the current goal.

We prove the intermediate claim Hinvlt2: Rlt (inv_nat n0) d1.

We prove the intermediate claim Hn0def: n0 = ordsucc N.

Use reflexivity.

rewrite the current goal using Hn0def (from left to right).

rewrite the current goal using Hd1eq (from left to right).

An exact proof term for the current goal is Hinvlt.

An exact proof term for the current goal is Hinvlt2.

We prove the intermediate claim Hp01w: order_rel (setprod R R) p01 w.

rewrite the current goal using Hp01def (from left to right).

Apply (order_rel_setprod_R_R_intro 0 1 (inv_nat n0) 0) to the current goal.

Apply orIL to the current goal.

An exact proof term for the current goal is (inv_nat_pos n0 Hn0In).

We prove the intermediate claim Ha0RR: a0 ∈ setprod R R.

An exact proof term for the current goal is ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) a0 Ha0Sq).

We prove the intermediate claim Hp01RR: p01 ∈ setprod R R.

An exact proof term for the current goal is ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) p01 Hp01Sq).

We prove the intermediate claim HwRR: w ∈ setprod R R.

An exact proof term for the current goal is ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) w HwSq).

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 p01 w simply_ordered_set_setprod_R_R Ha0RR Hp01RR HwRR Ha0p01 Hp01w).

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 ∧ order_rel (setprod R R) x0 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 Hwltb0.

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 HwUcap: w ∈ U ∩ ordsq_A.

An exact proof term for the current goal is (binintersectI U ordsq_A w HwU HwA).

An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_A) w HwUcap).

Assume Heq: c1 = d1 ∧ Rlt c2 d2.

Apply FalseE to the current goal.

We prove the intermediate claim H1lt: Rlt 1 d2.

rewrite the current goal using Hc2eq (from right to left) at position 1.

An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Heq).

We prove the intermediate claim Hd2eq: d2 = (b0 1).

We will prove d2 = (b0 1).

rewrite the current goal using (tuple_2_1_eq d1 d2) (from right to left) at position 1.

rewrite the current goal using Hb0Eq (from right to left) at position 1.

Use reflexivity.

We prove the intermediate claim Hb0yU: b0 1 ∈ 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 Hb0yprop0: ¬ (Rlt 1 (b0 1)).

An exact proof term for the current goal is (andER (¬ (Rlt (b0 1) 0)) (¬ (Rlt 1 (b0 1))) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (b0 1) Hb0yU)).

We prove the intermediate claim Hb0yprop: ¬ (Rlt 1 d2).

rewrite the current goal using Hd2eq (from left to right).

An exact proof term for the current goal is Hb0yprop0.

An exact proof term for the current goal is (Hb0yprop H1lt).

Assume HIlow: I ∈ Blow.

We prove the intermediate claim HIlow_ex: ∃b0 ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) x b0}.

An exact proof term for the current goal is (SepE2 (𝒫 ordered_square) (λJ0 : set ⇒ ∃b0 ∈ ordered_square, J0 = {x ∈ ordered_square|order_rel (setprod R R) x b0}) I HIlow).

Apply HIlow_ex to the current goal.

Let b0 be given.

Assume Hb0pack.

Apply Hb0pack to the current goal.

Assume Hb0Sq HeqI.

We prove the intermediate claim Hp01I2: p01 ∈ {x ∈ ordered_square|order_rel (setprod R R) x b0}.

rewrite the current goal using HeqI (from right to left).

An exact proof term for the current goal is Hp01I.

We prove the intermediate claim Hp01b0: order_rel (setprod R R) p01 b0.

An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) x0 b0) p01 Hp01I2).