Let p be given.

Assume Hpcl: 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 (λx0 : set ⇒ ∀U : set, U ∈ ordered_square_topology → x0 ∈ U → U ∩ ordsq_C ≠ Empty) p Hpcl).

We prove the intermediate claim Hcond: ∀U : set, U ∈ ordered_square_topology → p ∈ U → U ∩ ordsq_C ≠ Empty.

An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ ∀U : set, U ∈ ordered_square_topology → x0 ∈ U → U ∩ ordsq_C ≠ Empty) p Hpcl).

Set a to be the term p 0.

Set y to be the term p 1.

We prove the intermediate claim HaU: a ∈ unit_interval.

An exact proof term for the current goal is (ap0_Sigma unit_interval (λ_ : set ⇒ unit_interval) p HpSq).

We prove the intermediate claim HyU: y ∈ unit_interval.

An exact proof term for the current goal is (ap1_Sigma unit_interval (λ_ : set ⇒ unit_interval) p HpSq).

We prove the intermediate claim HaR: a ∈ R.

An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) a HaU).

We prove the intermediate claim HyR: y ∈ R.

An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) y HyU).

We prove the intermediate claim HaS: SNo a.

An exact proof term for the current goal is (real_SNo a HaR).

We prove the intermediate claim HyS: SNo y.

An exact proof term for the current goal is (real_SNo y HyR).

We prove the intermediate claim HpEta: p = (a,y).

An exact proof term for the current goal is (setprod_eta unit_interval unit_interval p HpSq).

Apply (SNoLt_trichotomy_or_impred y 0 HyS SNo_0 (p ∈ ordsq_C_closure)) to the current goal.

Assume Hylt0: y < 0.

Apply FalseE to the current goal.

We prove the intermediate claim Hylt0R: Rlt y 0.

An exact proof term for the current goal is (RltI y 0 HyR real_0 Hylt0).

An exact proof term for the current goal is ((andEL (¬ (Rlt y 0)) (¬ (Rlt 1 y)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) y HyU)) Hylt0R).

Assume Hyeq0: y = 0.

Apply (SNoLt_trichotomy_or_impred a 1 HaS SNo_1 (p ∈ ordsq_C_closure)) to the current goal.

Assume Halt1: a < 1.

Apply (SNoLt_trichotomy_or_impred a 0 HaS SNo_0 (p ∈ ordsq_C_closure)) to the current goal.

Assume Halt0: a < 0.

Apply FalseE to the current goal.

We prove the intermediate claim Halt0R: Rlt a 0.

An exact proof term for the current goal is (RltI a 0 HaR real_0 Halt0).

An exact proof term for the current goal is ((andEL (¬ (Rlt a 0)) (¬ (Rlt 1 a)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) a HaU)) Halt0R).

Assume Haeq0: a = 0.

Apply FalseE to the current goal.

Set b0 to be the term (0,eps_ 1).

Set U0 to be the term {x ∈ ordered_square|order_rel (setprod R R) x b0}.

We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 ordered_square.

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

We prove the intermediate claim Hb0Sq: b0 ∈ ordered_square.

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

We prove the intermediate claim HU0basis: U0 ∈ ordered_square_order_basis.

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

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

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

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

Use reflexivity.

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

Apply binunionI1 to the current goal.

Apply binunionI2 to the current goal.

We will prove U0 ∈ Blow.

Apply (SepI (𝒫 ordered_square) (λI : set ⇒ ∃b ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) x b}) U0) to the current goal.

An exact proof term for the current goal is HU0Pow.

We use b0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hb0Sq.

Use reflexivity.

We prove the intermediate claim HU0top: U0 ∈ ordered_square_topology.

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 left to right).

An exact proof term for the current goal is (generated_topology_contains_elem ordered_square ordered_square_order_basis U0 HU0Pow HU0basis).

We prove the intermediate claim HpOrd: order_rel (setprod R R) p b0.

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

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

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

Apply (order_rel_setprod_R_R_intro 0 0 0 (eps_ 1)) to the current goal.

Apply orIR to the current goal.

We prove the intermediate claim Hcore: 0 = 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 Hcore.

We prove the intermediate claim HpU0: p ∈ U0.

Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) x0 b0) p HpSq) to the current goal.

An exact proof term for the current goal is HpOrd.

We prove the intermediate claim HcapSub: U0 ∩ ordsq_C ⊆ Empty.

Let z be given.

Assume Hz: z ∈ U0 ∩ ordsq_C.

We will prove z ∈ Empty.

Apply FalseE to the current goal.

We prove the intermediate claim HzU: z ∈ U0.

An exact proof term for the current goal is (binintersectE1 U0 ordsq_C z Hz).

We prove the intermediate claim HzC: z ∈ ordsq_C.

An exact proof term for the current goal is (binintersectE2 U0 ordsq_C z Hz).

We prove the intermediate claim HzOrd: order_rel (setprod R R) z b0.

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

We prove the intermediate claim HzEx: ∃x0 : set, z = (x0,0) ∧ Rlt 0 x0 ∧ Rlt x0 1.

An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,0) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzC).

Apply HzEx to the current goal.

Let x0 be given.

Assume Hx0pack.

Apply Hx0pack to the current goal.

Assume Hcore Hx0lt1.

Apply Hcore to the current goal.

Assume HzEq H0ltx0.

We prove the intermediate claim Hnotx00: ¬ (Rlt x0 0).

An exact proof term for the current goal is (not_Rlt_sym 0 x0 H0ltx0).

We prove the intermediate claim Hx0R: x0 ∈ R.

An exact proof term for the current goal is (RltE_right 0 x0 H0ltx0).

We prove the intermediate claim HUnf: ∃a1 a2 b1 b2 : set, z = (a1,a2) ∧ b0 = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).

An exact proof term for the current goal is (order_rel_setprod_R_R_unfold z b0 HzOrd).

Apply HUnf to the current goal.

Let a1 be given.

Assume Ha2.

Apply Ha2 to the current goal.

Let a2 be given.

Assume Hb1.

Apply Hb1 to the current goal.

Let b1 be given.

Assume Hb2.

Apply Hb2 to the current goal.

Let b2 be given.

Assume Hcore2.

Apply Hcore2 to the current goal.

Assume Hpair Hdisj.

Apply Hpair to the current goal.

Assume HzEq2 Hb0Eq2.

We prove the intermediate claim Hzpair: (x0,0) = (a1,a2).

We will prove (x0,0) = (a1,a2).

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

An exact proof term for the current goal is HzEq2.

We prove the intermediate claim HzCoords: x0 = a1 ∧ 0 = a2.

An exact proof term for the current goal is (tuple_eq_coords x0 0 a1 a2 Hzpair).

We prove the intermediate claim Hx0eq: x0 = a1.

An exact proof term for the current goal is (andEL (x0 = a1) (0 = a2) HzCoords).

We prove the intermediate claim H0eq: 0 = a2.

An exact proof term for the current goal is (andER (x0 = a1) (0 = a2) HzCoords).

We prove the intermediate claim Hb0pair: (0,eps_ 1) = (b1,b2).

We will prove (0,eps_ 1) = (b1,b2).

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

Use reflexivity.

We prove the intermediate claim Hb0Coords: 0 = b1 ∧ (eps_ 1) = b2.

An exact proof term for the current goal is (tuple_eq_coords 0 (eps_ 1) b1 b2 Hb0pair).

We prove the intermediate claim Hb1eq: 0 = b1.

An exact proof term for the current goal is (andEL (0 = b1) ((eps_ 1) = b2) Hb0Coords).

Apply Hdisj to the current goal.

Assume Hlt: Rlt a1 b1.

Apply FalseE to the current goal.

We prove the intermediate claim Hx0lt0: Rlt x0 0.

We will prove Rlt x0 0.

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

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

An exact proof term for the current goal is Hlt.

An exact proof term for the current goal is (Hnotx00 Hx0lt0).

Assume Heq: a1 = b1 ∧ Rlt a2 b2.

Apply FalseE to the current goal.

We prove the intermediate claim Ha1eq: a1 = b1.

An exact proof term for the current goal is (andEL (a1 = b1) (Rlt a2 b2) Heq).

We prove the intermediate claim Hx0eq0: x0 = 0.

We will prove x0 = 0.

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

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

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

Use reflexivity.

We prove the intermediate claim Hbad: Rlt 0 0.

We will prove Rlt 0 0.

rewrite the current goal using Hx0eq0 (from right to left) at position 2.

An exact proof term for the current goal is H0ltx0.

An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) Hbad).

We prove the intermediate claim HcapEq: U0 ∩ ordsq_C = Empty.

An exact proof term for the current goal is (Empty_Subq_eq (U0 ∩ ordsq_C) HcapSub).

An exact proof term for the current goal is ((Hcond U0 HU0top HpU0) HcapEq).

Assume H0lta: 0 < a.

We prove the intermediate claim HpEq0: p = (a,0).

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

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

Use reflexivity.

We prove the intermediate claim HpC: p ∈ ordsq_C.

Apply (SepI ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,0) ∧ Rlt 0 x0 ∧ Rlt x0 1) p HpSq) to the current goal.

We use a to witness the existential quantifier.

We will prove p = (a,0) ∧ Rlt 0 a ∧ Rlt a 1.

Apply andI to the current goal.

We will prove p = (a,0) ∧ Rlt 0 a.

Apply andI to the current goal.

An exact proof term for the current goal is HpEq0.

An exact proof term for the current goal is (RltI 0 a real_0 HaR H0lta).

An exact proof term for the current goal is (RltI a 1 HaR real_1 Halt1).

Apply (binunionI1 (ordsq_C ∪ ordsq_top_edge_lt1) {ordsq_p10} p) to the current goal.

Apply (binunionI1 ordsq_C ordsq_top_edge_lt1 p) to the current goal.

An exact proof term for the current goal is HpC.

Assume Haeq1: a = 1.

Apply (binunionI2 (ordsq_C ∪ ordsq_top_edge_lt1) {ordsq_p10} p) to the current goal.

We prove the intermediate claim Hp10def: ordsq_p10 = (1,0).

Use reflexivity.

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

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

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

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

Apply SingI to the current goal.

Assume H1lta: 1 < a.

Apply FalseE to the current goal.

We prove the intermediate claim H1ltaR: Rlt 1 a.

An exact proof term for the current goal is (RltI 1 a real_1 HaR H1lta).

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

Assume H0lty: 0 < y.

Apply (SNoLt_trichotomy_or_impred y 1 HyS SNo_1 (p ∈ ordsq_C_closure)) to the current goal.

Assume Hylt1: y < 1.

Apply FalseE to the current goal.

We prove the intermediate claim H0y: Rlt 0 y.

An exact proof term for the current goal is (RltI 0 y real_0 HyR H0lty).

We prove the intermediate claim Hy1: Rlt y 1.

An exact proof term for the current goal is (RltI y 1 HyR real_1 Hylt1).

We prove the intermediate claim Hq1ex: ∃q1 ∈ rational_numbers, Rlt 0 q1 ∧ Rlt q1 y.

An exact proof term for the current goal is (rational_dense_between_reals 0 y real_0 HyR H0y).

Apply Hq1ex to the current goal.

Let q1 be given.

Assume Hq1pack.

Apply Hq1pack to the current goal.

Assume Hq1Q Hq1ineq.

We prove the intermediate claim H0ltq1: Rlt 0 q1.

An exact proof term for the current goal is (andEL (Rlt 0 q1) (Rlt q1 y) Hq1ineq).

We prove the intermediate claim Hq1lty: Rlt q1 y.

An exact proof term for the current goal is (andER (Rlt 0 q1) (Rlt q1 y) Hq1ineq).

We prove the intermediate claim Hq2ex: ∃q2 ∈ rational_numbers, Rlt y q2 ∧ Rlt q2 1.

An exact proof term for the current goal is (rational_dense_between_reals y 1 HyR real_1 Hy1).

Apply Hq2ex to the current goal.

Let q2 be given.

Assume Hq2pack.

Apply Hq2pack to the current goal.

Assume Hq2Q Hq2ineq.

We prove the intermediate claim Hylq2: Rlt y q2.

An exact proof term for the current goal is (andEL (Rlt y q2) (Rlt q2 1) Hq2ineq).

We prove the intermediate claim Hq2lt1: Rlt q2 1.

An exact proof term for the current goal is (andER (Rlt y q2) (Rlt q2 1) Hq2ineq).

We prove the intermediate claim Hq1R: q1 ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q1 Hq1Q).

We prove the intermediate claim Hq2R: q2 ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q2 Hq2Q).

We prove the intermediate claim Hq1lt1: Rlt q1 1.

An exact proof term for the current goal is (Rlt_tra q1 y 1 Hq1lty Hy1).

We prove the intermediate claim H0ltq2: Rlt 0 q2.

An exact proof term for the current goal is (Rlt_tra 0 y q2 H0y Hylq2).

We prove the intermediate claim Hnotq10: ¬ (Rlt q1 0).

An exact proof term for the current goal is (not_Rlt_sym 0 q1 H0ltq1).

We prove the intermediate claim Hnot1q1: ¬ (Rlt 1 q1).

An exact proof term for the current goal is (not_Rlt_sym q1 1 Hq1lt1).

We prove the intermediate claim Hnotq20: ¬ (Rlt q2 0).

An exact proof term for the current goal is (not_Rlt_sym 0 q2 H0ltq2).

We prove the intermediate claim Hnot1q2: ¬ (Rlt 1 q2).

An exact proof term for the current goal is (not_Rlt_sym q2 1 Hq2lt1).

We prove the intermediate claim Hq1U: q1 ∈ unit_interval.

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

Apply andI to the current goal.

An exact proof term for the current goal is Hnotq10.

An exact proof term for the current goal is Hnot1q1.

We prove the intermediate claim Hq2U: q2 ∈ unit_interval.

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

Apply andI to the current goal.

An exact proof term for the current goal is Hnotq20.

An exact proof term for the current goal is Hnot1q2.

Set pL to be the term (a,q1).

Set pU to be the term (a,q2).

We prove the intermediate claim HpLSq: pL ∈ ordered_square.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval a q1 HaU Hq1U).

We prove the intermediate claim HpUSq: pU ∈ ordered_square.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval a q2 HaU Hq2U).

We prove the intermediate claim HpLdef: pL = (a,q1).

Use reflexivity.

We prove the intermediate claim HpUdef: pU = (a,q2).

Use reflexivity.

Set U0 to be the term {x ∈ ordered_square|order_rel (setprod R R) pL x ∧ order_rel (setprod R R) x pU}.

We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 ordered_square.

An exact proof term for the current goal is (Sep_In_Power ordered_square (λx0 : set ⇒ order_rel (setprod R R) pL x0 ∧ order_rel (setprod R R) x0 pU)).

We prove the intermediate claim HU0basis: U0 ∈ ordered_square_order_basis.

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

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

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

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

Use reflexivity.

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

Apply binunionI1 to the current goal.

We will prove U0 ∈ Bint.

Apply (SepI (𝒫 ordered_square) (λI : set ⇒ ∃a0 ∈ ordered_square, ∃b ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) a0 x ∧ order_rel (setprod R R) x b}) U0) to the current goal.

An exact proof term for the current goal is HU0Pow.

We use pL to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HpLSq.

We use pU to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HpUSq.

Use reflexivity.

We prove the intermediate claim HU0top: U0 ∈ ordered_square_topology.

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 left to right).

An exact proof term for the current goal is (generated_topology_contains_elem ordered_square ordered_square_order_basis U0 HU0Pow HU0basis).

We prove the intermediate claim HpLtp: order_rel (setprod R R) pL p.

We prove the intermediate claim HpEta01: p = (p 0,p 1).

An exact proof term for the current goal is (setprod_eta unit_interval unit_interval p HpSq).

We prove the intermediate claim HyDef: y = p 1.

Use reflexivity.

We prove the intermediate claim Hq1ltp1: Rlt q1 (p 1).

We will prove Rlt q1 (p 1).

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

An exact proof term for the current goal is Hq1lty.

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

rewrite the current goal using HpEta01 (from left to right) at position 2.

We prove the intermediate claim Hcore: a = (p 0) ∧ Rlt q1 (p 1).

Apply andI to the current goal.

Use reflexivity.

An exact proof term for the current goal is Hq1ltp1.

An exact proof term for the current goal is (order_rel_setprod_R_R_intro a q1 (p 0) (p 1) (orIR (Rlt a (p 0)) (a = (p 0) ∧ Rlt q1 (p 1)) Hcore)).

We prove the intermediate claim HptpU: order_rel (setprod R R) p pU.

We prove the intermediate claim HpEta01: p = (p 0,p 1).

An exact proof term for the current goal is (setprod_eta unit_interval unit_interval p HpSq).

We prove the intermediate claim HaDef: a = p 0.

Use reflexivity.

We prove the intermediate claim HyDef: y = p 1.

Use reflexivity.

We prove the intermediate claim Hp0eqa: (p 0) = a.

We will prove (p 0) = a.

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

Use reflexivity.

We prove the intermediate claim Hp1ltq2: Rlt (p 1) q2.

We will prove Rlt (p 1) q2.

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

An exact proof term for the current goal is Hylq2.

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

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

We prove the intermediate claim Hcore: (p 0) = a ∧ Rlt (p 1) q2.

Apply andI to the current goal.

An exact proof term for the current goal is Hp0eqa.

An exact proof term for the current goal is Hp1ltq2.

An exact proof term for the current goal is (order_rel_setprod_R_R_intro (p 0) (p 1) a q2 (orIR (Rlt (p 0) a) ((p 0) = a ∧ Rlt (p 1) q2) Hcore)).

We prove the intermediate claim HpU0: p ∈ U0.

Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) pL x0 ∧ order_rel (setprod R R) x0 pU) p HpSq) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is HpLtp.

An exact proof term for the current goal is HptpU.

We prove the intermediate claim HcapSub: U0 ∩ ordsq_C ⊆ Empty.

Let z be given.

Assume Hz: z ∈ U0 ∩ ordsq_C.

We will prove z ∈ Empty.

Apply FalseE to the current goal.

We prove the intermediate claim HzU: z ∈ U0.

An exact proof term for the current goal is (binintersectE1 U0 ordsq_C z Hz).

We prove the intermediate claim HzC: z ∈ ordsq_C.

An exact proof term for the current goal is (binintersectE2 U0 ordsq_C z Hz).

We prove the intermediate claim HzUcond: order_rel (setprod R R) pL z ∧ order_rel (setprod R R) z pU.

An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) pL x0 ∧ order_rel (setprod R R) x0 pU) z HzU).

We prove the intermediate claim HpLz: order_rel (setprod R R) pL z.

An exact proof term for the current goal is (andEL (order_rel (setprod R R) pL z) (order_rel (setprod R R) z pU) HzUcond).

We prove the intermediate claim HzpU: order_rel (setprod R R) z pU.

An exact proof term for the current goal is (andER (order_rel (setprod R R) pL z) (order_rel (setprod R R) z pU) HzUcond).

We prove the intermediate claim HzEx: ∃x0 : set, z = (x0,0) ∧ Rlt 0 x0 ∧ Rlt x0 1.

An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,0) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzC).

Apply HzEx to the current goal.

Let x0 be given.

Assume Hx0pack.

Apply Hx0pack to the current goal.

Assume Hcore Hx0lt1.

Apply Hcore to the current goal.

Assume HzEq H0ltx0.

We prove the intermediate claim Hx0R: x0 ∈ R.

An exact proof term for the current goal is (RltE_right 0 x0 H0ltx0).

We prove the intermediate claim HpLzUnf: ∃a1 a2 b1 b2 : set, pL = (a1,a2) ∧ z = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).

An exact proof term for the current goal is (order_rel_setprod_R_R_unfold pL z HpLz).

We prove the intermediate claim HaLtX0: Rlt a x0.

Apply HpLzUnf to the current goal.

Let a1 be given.

Assume Ha2.

Apply Ha2 to the current goal.

Let a2 be given.

Assume Hb1.

Apply Hb1 to the current goal.

Let b1 be given.

Assume Hb2.

Apply Hb2 to the current goal.

Let b2 be given.

Assume Hcore.

Apply Hcore to the current goal.

Assume Hpair Hdisj.

Apply Hpair to the current goal.

Assume HpLeq HzEq2.

We prove the intermediate claim HpLpair: (a,q1) = (a1,a2).

We will prove (a,q1) = (a1,a2).

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

An exact proof term for the current goal is HpLeq.

We prove the intermediate claim HaCoords: a = a1 ∧ q1 = a2.

An exact proof term for the current goal is (tuple_eq_coords a q1 a1 a2 HpLpair).

We prove the intermediate claim Haeq: a = a1.

An exact proof term for the current goal is (andEL (a = a1) (q1 = a2) HaCoords).

We prove the intermediate claim Hq1eq: q1 = a2.

An exact proof term for the current goal is (andER (a = a1) (q1 = a2) HaCoords).

We prove the intermediate claim Hzpair: (x0,0) = (b1,b2).

We will prove (x0,0) = (b1,b2).

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

An exact proof term for the current goal is HzEq2.

We prove the intermediate claim HzCoords: x0 = b1 ∧ 0 = b2.

An exact proof term for the current goal is (tuple_eq_coords x0 0 b1 b2 Hzpair).

We prove the intermediate claim Hx0eq: x0 = b1.

An exact proof term for the current goal is (andEL (x0 = b1) (0 = b2) HzCoords).

We prove the intermediate claim H0eq: 0 = b2.

An exact proof term for the current goal is (andER (x0 = b1) (0 = b2) HzCoords).

Apply Hdisj to the current goal.

Assume Hlt: Rlt a1 b1.

We will prove Rlt a x0.

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

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

An exact proof term for the current goal is Hlt.

Assume Heq: a1 = b1 ∧ Rlt a2 b2.

Apply FalseE to the current goal.

We prove the intermediate claim HltA2B2: Rlt a2 b2.

An exact proof term for the current goal is (andER (a1 = b1) (Rlt a2 b2) Heq).

We prove the intermediate claim Ha2eq: a2 = q1.

We will prove a2 = q1.

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

Use reflexivity.

We prove the intermediate claim Hb2eq: b2 = 0.

We will prove b2 = 0.

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

Use reflexivity.

We prove the intermediate claim Hq1lt0: Rlt q1 0.

We will prove Rlt q1 0.

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

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

An exact proof term for the current goal is HltA2B2.

An exact proof term for the current goal is (Hnotq10 Hq1lt0).

We prove the intermediate claim HzpUUnf: ∃a1 a2 b1 b2 : set, z = (a1,a2) ∧ pU = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).

An exact proof term for the current goal is (order_rel_setprod_R_R_unfold z pU HzpU).

Apply HzpUUnf to the current goal.

Let a1 be given.

Assume Ha2.

Apply Ha2 to the current goal.

Let a2 be given.

Assume Hb1.

Apply Hb1 to the current goal.

Let b1 be given.

Assume Hb2.

Apply Hb2 to the current goal.

Let b2 be given.

Assume Hcore.

Apply Hcore to the current goal.

Assume Hpair Hdisj.

Apply Hpair to the current goal.

Assume HzEq2 HpUeq.

We prove the intermediate claim Hzpair: (x0,0) = (a1,a2).

We will prove (x0,0) = (a1,a2).

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

An exact proof term for the current goal is HzEq2.

We prove the intermediate claim HzCoords: x0 = a1 ∧ 0 = a2.

An exact proof term for the current goal is (tuple_eq_coords x0 0 a1 a2 Hzpair).

We prove the intermediate claim Hx0eq: x0 = a1.

An exact proof term for the current goal is (andEL (x0 = a1) (0 = a2) HzCoords).

We prove the intermediate claim H0eq: 0 = a2.

An exact proof term for the current goal is (andER (x0 = a1) (0 = a2) HzCoords).

We prove the intermediate claim HpUpair: (a,q2) = (b1,b2).

We will prove (a,q2) = (b1,b2).

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

An exact proof term for the current goal is HpUeq.

We prove the intermediate claim HpUCoords: a = b1 ∧ q2 = b2.

An exact proof term for the current goal is (tuple_eq_coords a q2 b1 b2 HpUpair).

We prove the intermediate claim Haeq: a = b1.

An exact proof term for the current goal is (andEL (a = b1) (q2 = b2) HpUCoords).

We prove the intermediate claim Hq2eq: q2 = b2.

An exact proof term for the current goal is (andER (a = b1) (q2 = b2) HpUCoords).

Apply Hdisj to the current goal.

Assume Hlt: Rlt a1 b1.

Apply FalseE to the current goal.

We prove the intermediate claim Hbad: Rlt a a.

We prove the intermediate claim Hx0ltb1: Rlt x0 b1.

We will prove Rlt x0 b1.

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

An exact proof term for the current goal is Hlt.

We prove the intermediate claim Hab1: Rlt a b1.

An exact proof term for the current goal is (Rlt_tra a x0 b1 HaLtX0 Hx0ltb1).

We will prove Rlt a a.

rewrite the current goal using Haeq (from left to right) at position 2.

An exact proof term for the current goal is Hab1.

An exact proof term for the current goal is ((not_Rlt_refl a HaR) Hbad).

Assume Heq: a1 = b1 ∧ Rlt a2 b2.

Apply FalseE to the current goal.

We prove the intermediate claim Hx0eqA: x0 = a.

We will prove x0 = a.

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

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

An exact proof term for the current goal is (andEL (a1 = b1) (Rlt a2 b2) Heq).

We prove the intermediate claim Hbad: Rlt a a.

We will prove Rlt a a.

rewrite the current goal using Hx0eqA (from right to left) at position 2.

An exact proof term for the current goal is HaLtX0.

An exact proof term for the current goal is ((not_Rlt_refl a HaR) Hbad).

We prove the intermediate claim HcapEq: U0 ∩ ordsq_C = Empty.

An exact proof term for the current goal is (Empty_Subq_eq (U0 ∩ ordsq_C) HcapSub).

An exact proof term for the current goal is ((Hcond U0 HU0top HpU0) HcapEq).

Assume Hyeq1: y = 1.

Apply (SNoLt_trichotomy_or_impred a 1 HaS SNo_1 (p ∈ ordsq_C_closure)) to the current goal.

Assume Halt1: a < 1.

Apply (binunionI1 (ordsq_C ∪ ordsq_top_edge_lt1) {ordsq_p10} p) to the current goal.

Apply (binunionI2 ordsq_C ordsq_top_edge_lt1 p) to the current goal.

Apply (SepI ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,1) ∧ x0 ∈ unit_interval ∧ Rlt x0 1) p HpSq) to the current goal.

We use a to witness the existential quantifier.

We will prove p = (a,1) ∧ a ∈ unit_interval ∧ Rlt a 1.

Apply andI to the current goal.

We will prove p = (a,1) ∧ a ∈ unit_interval.

Apply andI to the current goal.

rewrite the current goal using Hyeq1 (from right to left) at position 2.

An exact proof term for the current goal is HpEta.

An exact proof term for the current goal is HaU.

An exact proof term for the current goal is (RltI a 1 HaR real_1 Halt1).

Assume Haeq1: a = 1.

Apply FalseE to the current goal.

Set U0 to be the term {x ∈ ordered_square|order_rel (setprod R R) ordsq_p10 x}.

We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 ordered_square.

An exact proof term for the current goal is (Sep_In_Power ordered_square (λx0 : set ⇒ order_rel (setprod R R) ordsq_p10 x0)).

We prove the intermediate claim Hp10Sq: ordsq_p10 ∈ ordered_square.

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 HU0basis: U0 ∈ ordered_square_order_basis.

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

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

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

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

Use reflexivity.

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

Apply binunionI2 to the current goal.

We will prove U0 ∈ Bup.

Apply (SepI (𝒫 ordered_square) (λI : set ⇒ ∃a0 ∈ ordered_square, I = {x ∈ ordered_square|order_rel (setprod R R) a0 x}) U0) to the current goal.

An exact proof term for the current goal is HU0Pow.

We use ordsq_p10 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hp10Sq.

Use reflexivity.

We prove the intermediate claim HU0top: U0 ∈ ordered_square_topology.

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 left to right).

An exact proof term for the current goal is (generated_topology_contains_elem ordered_square ordered_square_order_basis U0 HU0Pow HU0basis).

We prove the intermediate claim HpOrd: order_rel (setprod R R) ordsq_p10 p.

We prove the intermediate claim Hp10def: ordsq_p10 = (1,0).

Use reflexivity.

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

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

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

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

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

Apply orIR to the current goal.

We will prove 1 = 1 ∧ Rlt 0 1.

Apply andI to the current goal.

Use reflexivity.

An exact proof term for the current goal is Rlt_0_1.

We prove the intermediate claim HpU0: p ∈ U0.

Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) ordsq_p10 x0) p HpSq) to the current goal.

An exact proof term for the current goal is HpOrd.

We prove the intermediate claim HcapSub: U0 ∩ ordsq_C ⊆ Empty.

Let z be given.

Assume Hz: z ∈ U0 ∩ ordsq_C.

We will prove z ∈ Empty.

Apply FalseE to the current goal.

We prove the intermediate claim HzU: z ∈ U0.

An exact proof term for the current goal is (binintersectE1 U0 ordsq_C z Hz).

We prove the intermediate claim HzC: z ∈ ordsq_C.

An exact proof term for the current goal is (binintersectE2 U0 ordsq_C z Hz).

We prove the intermediate claim HzSq: z ∈ ordered_square.

An exact proof term for the current goal is (SepE1 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,0) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzC).

We prove the intermediate claim HzOrd: order_rel (setprod R R) ordsq_p10 z.

An exact proof term for the current goal is (SepE2 ordered_square (λx0 : set ⇒ order_rel (setprod R R) ordsq_p10 x0) z HzU).

We prove the intermediate claim HzEx: ∃x0 : set, z = (x0,0) ∧ Rlt 0 x0 ∧ Rlt x0 1.

An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,0) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzC).

Apply HzEx to the current goal.

Let x0 be given.

Assume Hx0pack.

Apply Hx0pack to the current goal.

Assume Hcore Hx0lt1.

Apply Hcore to the current goal.

Assume HzEq H0ltx0.

We prove the intermediate claim HzRR: z ∈ 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) z HzSq).

We prove the intermediate claim Hp10RR: ordsq_p10 ∈ 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) ordsq_p10 Hp10Sq).

We prove the intermediate claim Hzltp10: order_rel (setprod R R) z ordsq_p10.

We prove the intermediate claim Hp10def: ordsq_p10 = (1,0).

Use reflexivity.

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

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

Apply (order_rel_setprod_R_R_intro x0 0 1 0) to the current goal.

Apply orIL to the current goal.

An exact proof term for the current goal is Hx0lt1.

We prove the intermediate claim Hp10p10: order_rel (setprod R R) ordsq_p10 ordsq_p10.

An exact proof term for the current goal is (order_rel_trans (setprod R R) ordsq_p10 z ordsq_p10 simply_ordered_set_setprod_R_R Hp10RR HzRR Hp10RR HzOrd Hzltp10).

An exact proof term for the current goal is ((order_rel_irref (setprod R R) ordsq_p10) Hp10p10).

We prove the intermediate claim HcapEq: U0 ∩ ordsq_C = Empty.

An exact proof term for the current goal is (Empty_Subq_eq (U0 ∩ ordsq_C) HcapSub).

An exact proof term for the current goal is ((Hcond U0 HU0top HpU0) HcapEq).

Assume H1lta: 1 < a.

Apply FalseE to the current goal.

We prove the intermediate claim H1ltaR: Rlt 1 a.

An exact proof term for the current goal is (RltI 1 a real_1 HaR H1lta).

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

Assume H1lty: 1 < y.

Apply FalseE to the current goal.

We prove the intermediate claim H1ltyR: Rlt 1 y.

An exact proof term for the current goal is (RltI 1 y real_1 HyR H1lty).

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