We will prove closure_of ordered_square ordered_square_topology ordsq_D = ordsq_D_closure.
Apply set_ext to the current goal.
Let p be given.
Assume Hpcl: p ∈ closure_of ordered_square ordered_square_topology ordsq_D.
We will prove p ∈ ordsq_D_closure.
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_D ≠ Empty) p Hpcl).
We prove the intermediate claim Hcond: ∀U : set, U ∈ ordered_square_topology → p ∈ U → U ∩ ordsq_D ≠ 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_D ≠ Empty) p Hpcl).
Set x to be the term p 0.
Set y to be the term p 1.
We prove the intermediate claim HpEta: p = (x,y).
An exact proof term for the current goal is (setprod_eta unit_interval 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 HxU: x ∈ 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 HyR: y ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R y HyU).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R x HxU).
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 HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
Apply (xm (y = eps_ 1)) to the current goal.
Assume Hyeps: y = eps_ 1.
Apply (xm (x = 0)) to the current goal.
Assume Hx0: x = 0.
Apply FalseE to the current goal.
Set a to be the term (0,0).
Set b to be the term (0,1).
Set U0 to be the term {z ∈ ordered_square|order_rel (setprod R R) a z ∧ order_rel (setprod R R) z b}.
We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 ordered_square.
An exact proof term for the current goal is (Sep_In_Power ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b)).
Set Bint to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}}.
Set Blow to be the term {I ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}}.
Set Bup to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}}.
We prove the intermediate claim HU0basis: U0 ∈ ordered_square_order_basis.
We prove the intermediate claim HdefB: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).
Use reflexivity.
rewrite the current goal using HdefB (from left to right).
Apply binunionI1 to the current goal.
Apply binunionI1 to the current goal.
Apply (SepI (𝒫 ordered_square) (λI0 : set ⇒ ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I0 = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}) U0 HU0Pow) to the current goal.
We use a to witness the existential quantifier.
We will prove a ∈ ordered_square ∧ ∃b0 ∈ ordered_square, U0 = {x0 ∈ ordered_square|order_rel (setprod R R) a x0 ∧ order_rel (setprod R R) x0 b0}.
Apply andI to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval 0 0 zero_in_unit_interval zero_in_unit_interval).
We use b to witness the existential quantifier.
We will prove b ∈ ordered_square ∧ U0 = {x0 ∈ ordered_square|order_rel (setprod R R) a x0 ∧ order_rel (setprod R R) x0 b}.
Apply andI to the current goal.
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).
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 Hap: order_rel (setprod R R) a p.
rewrite the current goal using HpEta (from left to right).
rewrite the current goal using Hx0 (from left to right).
Apply (order_rel_setprod_R_R_intro 0 0 0 y) to the current goal.
Apply orIR to the current goal.
Apply andI to the current goal.
Use reflexivity.
rewrite the current goal using Hyeps (from left to right).
An exact proof term for the current goal is eps_1_pos_R.
We prove the intermediate claim Hpb: order_rel (setprod R R) p b.
rewrite the current goal using HpEta (from left to right) at position 1.
rewrite the current goal using Hx0 (from left to right).
Apply (order_rel_setprod_R_R_intro 0 y 0 1) to the current goal.
Apply orIR to the current goal.
Apply andI to the current goal.
Use reflexivity.
rewrite the current goal using Hyeps (from left to right) at position 1.
An exact proof term for the current goal is eps_1_lt1_R.
We prove the intermediate claim HpU0: p ∈ U0.
Apply (SepI ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b) p HpSq) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hap.
An exact proof term for the current goal is Hpb.
We prove the intermediate claim Hsub: U0 ∩ ordsq_D ⊆ Empty.
Let z be given.
Assume Hz: z ∈ U0 ∩ ordsq_D.
We will prove z ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HzU0: z ∈ U0.
An exact proof term for the current goal is (binintersectE1 U0 ordsq_D z Hz).
We prove the intermediate claim HzD: z ∈ ordsq_D.
An exact proof term for the current goal is (binintersectE2 U0 ordsq_D z Hz).
We prove the intermediate claim HzU0core: 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 (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b) z HzU0).
We prove the intermediate claim Hzltb: order_rel (setprod R R) z b.
An exact proof term for the current goal is (andER (order_rel (setprod R R) a z) (order_rel (setprod R R) z b) HzU0core).
We prove the intermediate claim HexD: ∃x0 : set, z = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1.
An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzD).
Apply HexD to the current goal.
Let x0 be given.
Assume Hx0pack.
Apply Hx0pack to the current goal.
Assume HcoreD Hx0lt1.
Apply HcoreD to the current goal.
Assume HzEq Hx0pos.
We prove the intermediate claim Hbltz: order_rel (setprod R R) b z.
rewrite the current goal using HzEq (from left to right).
Apply (order_rel_setprod_R_R_intro 0 1 x0 (eps_ 1)) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hx0pos.
We prove the intermediate claim HbR: b ∈ 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) b (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 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 (SepE1 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzD)).
We prove the intermediate claim Hbb: order_rel (setprod R R) b b.
An exact proof term for the current goal is (order_rel_trans (setprod R R) b z b simply_ordered_set_setprod_R_R HbR HzRR HbR Hbltz Hzltb).
An exact proof term for the current goal is ((order_rel_irref (setprod R R) b) Hbb).
We prove the intermediate claim HcapEq: U0 ∩ ordsq_D = Empty.
An exact proof term for the current goal is (Empty_Subq_eq (U0 ∩ ordsq_D) Hsub).
An exact proof term for the current goal is ((Hcond U0 HU0top HpU0) HcapEq).
Assume Hxn0: ¬ (x = 0).
Apply (xm (x = 1)) to the current goal.
Assume Hx1: x = 1.
Apply FalseE to the current goal.
Set a to be the term (1,0).
Set b to be the term (1,1).
Set U0 to be the term {z ∈ ordered_square|order_rel (setprod R R) a z ∧ order_rel (setprod R R) z b}.
We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 ordered_square.
An exact proof term for the current goal is (Sep_In_Power ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b)).
Set Bint to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}}.
Set Blow to be the term {I ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}}.
Set Bup to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}}.
We prove the intermediate claim HU0basis: U0 ∈ ordered_square_order_basis.
We prove the intermediate claim HdefB: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).
Use reflexivity.
rewrite the current goal using HdefB (from left to right).
Apply binunionI1 to the current goal.
Apply binunionI1 to the current goal.
Apply (SepI (𝒫 ordered_square) (λI0 : set ⇒ ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I0 = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}) U0 HU0Pow) to the current goal.
We use a to witness the existential quantifier.
We will prove a ∈ ordered_square ∧ ∃b0 ∈ ordered_square, U0 = {x0 ∈ ordered_square|order_rel (setprod R R) a x0 ∧ order_rel (setprod R R) x0 b0}.
Apply andI to the current goal.
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 use b to witness the existential quantifier.
We will prove b ∈ ordered_square ∧ U0 = {x0 ∈ ordered_square|order_rel (setprod R R) a x0 ∧ order_rel (setprod R R) x0 b}.
Apply andI to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval 1 1 one_in_unit_interval one_in_unit_interval).
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 Hap: order_rel (setprod R R) a p.
rewrite the current goal using HpEta (from left to right).
rewrite the current goal using Hx1 (from left to right).
Apply (order_rel_setprod_R_R_intro 1 0 1 y) to the current goal.
Apply orIR to the current goal.
Apply andI to the current goal.
Use reflexivity.
rewrite the current goal using Hyeps (from left to right).
An exact proof term for the current goal is eps_1_pos_R.
We prove the intermediate claim Hpb: order_rel (setprod R R) p b.
rewrite the current goal using HpEta (from left to right) at position 1.
rewrite the current goal using Hx1 (from left to right).
Apply (order_rel_setprod_R_R_intro 1 y 1 1) to the current goal.
Apply orIR to the current goal.
Apply andI to the current goal.
Use reflexivity.
rewrite the current goal using Hyeps (from left to right) at position 1.
An exact proof term for the current goal is eps_1_lt1_R.
We prove the intermediate claim HpU0: p ∈ U0.
Apply (SepI ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b) p HpSq) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hap.
An exact proof term for the current goal is Hpb.
We prove the intermediate claim Hsub: U0 ∩ ordsq_D ⊆ Empty.
Let z be given.
Assume Hz: z ∈ U0 ∩ ordsq_D.
We will prove z ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HzU0: z ∈ U0.
An exact proof term for the current goal is (binintersectE1 U0 ordsq_D z Hz).
We prove the intermediate claim HzD: z ∈ ordsq_D.
An exact proof term for the current goal is (binintersectE2 U0 ordsq_D z Hz).
We prove the intermediate claim HzU0core: 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 (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b) z HzU0).
We prove the intermediate claim Haltz: order_rel (setprod R R) a z.
An exact proof term for the current goal is (andEL (order_rel (setprod R R) a z) (order_rel (setprod R R) z b) HzU0core).
We prove the intermediate claim HexD: ∃x0 : set, z = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1.
An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzD).
Apply HexD to the current goal.
Let x0 be given.
Assume Hx0pack.
Apply Hx0pack to the current goal.
Assume HcoreD Hx0lt1.
Apply HcoreD to the current goal.
Assume HzEq Hx0pos.
We prove the intermediate claim Hzlta: order_rel (setprod R R) z a.
rewrite the current goal using HzEq (from left to right).
Apply (order_rel_setprod_R_R_intro x0 (eps_ 1) 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 HaR: a ∈ 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) a (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 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 (SepE1 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzD)).
We prove the intermediate claim Haa: order_rel (setprod R R) a a.
An exact proof term for the current goal is (order_rel_trans (setprod R R) a z a simply_ordered_set_setprod_R_R HaR HzRR HaR Haltz Hzlta).
An exact proof term for the current goal is ((order_rel_irref (setprod R R) a) Haa).
We prove the intermediate claim HcapEq: U0 ∩ ordsq_D = Empty.
An exact proof term for the current goal is (Empty_Subq_eq (U0 ∩ ordsq_D) Hsub).
An exact proof term for the current goal is ((Hcond U0 HU0top HpU0) HcapEq).
Assume Hxn1: ¬ (x = 1).
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 Hn1ltx: ¬ (Rlt 1 x).
An exact proof term for the current goal is (andER (¬ (Rlt x 0)) (¬ (Rlt 1 x)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) x HxU)).
We prove the intermediate claim Hxpos: Rlt 0 x.
Apply (SNoLt_trichotomy_or_impred x 0 HxS SNo_0 (Rlt 0 x)) 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.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxn0 Hxeq0).
Assume H0ltx: 0 < x.
An exact proof term for the current goal is (RltI 0 x real_0 HxR H0ltx).
We prove the intermediate claim Hxlt1: Rlt x 1.
Apply (SNoLt_trichotomy_or_impred 1 x SNo_1 HxS (Rlt x 1)) to the current goal.
Assume H1ltx: 1 < x.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hn1ltx (RltI 1 x real_1 HxR H1ltx)).
Assume H1eqx: 1 = x.
Apply FalseE to the current goal.
We prove the intermediate claim Hxeq1: x = 1.
rewrite the current goal using H1eqx (from right to left) at position 1.
Use reflexivity.
An exact proof term for the current goal is (Hxn1 Hxeq1).
Assume Hxlt1S: x < 1.
An exact proof term for the current goal is (RltI x 1 HxR real_1 Hxlt1S).
We prove the intermediate claim HpD: p ∈ ordsq_D.
Apply (SepI ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) p HpSq) to the current goal.
We use x to witness the existential quantifier.
We will prove (p = (x,eps_ 1) ∧ Rlt 0 x) ∧ Rlt x 1.
Apply andI to the current goal.
We will prove p = (x,eps_ 1) ∧ Rlt 0 x.
Apply andI to the current goal.
We will prove p = (x,eps_ 1).
rewrite the current goal using HpEta (from left to right) at position 1.
rewrite the current goal using Hyeps (from left to right) at position 1.
Use reflexivity.
An exact proof term for the current goal is Hxpos.
An exact proof term for the current goal is Hxlt1.
We prove the intermediate claim HdefDcl: ordsq_D_closure = ((ordsq_D ∪ ordsq_C) ∪ ordsq_top_edge_lt1) ∪ {ordsq_p10}.
Use reflexivity.
rewrite the current goal using HdefDcl (from left to right).
Apply binunionI1 to the current goal.
Apply binunionI1 to the current goal.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is HpD.
Assume HynEps: ¬ (y = eps_ 1).
Apply (xm (y = 0)) to the current goal.
Assume Hy0: y = 0.
Apply (xm (x = 1)) to the current goal.
Assume Hx1: x = 1.
We prove the intermediate claim HdefDcl: ordsq_D_closure = ((ordsq_D ∪ ordsq_C) ∪ ordsq_top_edge_lt1) ∪ {ordsq_p10}.
Use reflexivity.
rewrite the current goal using HdefDcl (from left to right).
Apply binunionI2 to the current goal.
We prove the intermediate claim HpEq: p = ordsq_p10.
We prove the intermediate claim Hp10def: ordsq_p10 = (1,0).
Use reflexivity.
rewrite the current goal using HpEta (from left to right).
rewrite the current goal using Hx1 (from left to right).
rewrite the current goal using Hy0 (from left to right).
rewrite the current goal using Hp10def (from right to left).
Use reflexivity.
rewrite the current goal using HpEq (from left to right).
An exact proof term for the current goal is (SingI ordsq_p10).
Assume Hxn1: ¬ (x = 1).
Apply (xm (x = 0)) to the current goal.
Assume Hx0: x = 0.
Apply FalseE to the current goal.
Set b to be the term (0,eps_ 1).
Set U0 to be the term {z ∈ ordered_square|order_rel (setprod R R) z b}.
We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 ordered_square.
An exact proof term for the current goal is (Sep_In_Power ordered_square (λz0 : set ⇒ order_rel (setprod R R) z0 b)).
Set Bint to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}}.
Set Blow to be the term {I ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}}.
Set Bup to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}}.
We prove the intermediate claim HU0basis: U0 ∈ ordered_square_order_basis.
We prove the intermediate claim HdefB: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).
Use reflexivity.
rewrite the current goal using HdefB (from left to right).
Apply binunionI1 to the current goal.
Apply binunionI2 to the current goal.
Apply (SepI (𝒫 ordered_square) (λI0 : set ⇒ ∃b0 ∈ ordered_square, I0 = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}) U0 HU0Pow) to the current goal.
We use b to witness the existential quantifier.
We will prove b ∈ ordered_square ∧ U0 = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b}.
Apply andI to the current goal.
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).
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 Hpb: order_rel (setprod R R) p b.
rewrite the current goal using HpEta (from left to right).
rewrite the current goal using Hx0 (from left to right).
rewrite the current goal using Hy0 (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.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is eps_1_pos_R.
We prove the intermediate claim HpU0: p ∈ U0.
Apply (SepI ordered_square (λz0 : set ⇒ order_rel (setprod R R) z0 b) p HpSq) to the current goal.
An exact proof term for the current goal is Hpb.
We prove the intermediate claim Hsub: U0 ∩ ordsq_D ⊆ Empty.
Let z be given.
Assume Hz: z ∈ U0 ∩ ordsq_D.
We will prove z ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HzU0: z ∈ U0.
An exact proof term for the current goal is (binintersectE1 U0 ordsq_D z Hz).
We prove the intermediate claim HzD: z ∈ ordsq_D.
An exact proof term for the current goal is (binintersectE2 U0 ordsq_D z Hz).
We prove the intermediate claim Hzltb: order_rel (setprod R R) z b.
An exact proof term for the current goal is (SepE2 ordered_square (λz0 : set ⇒ order_rel (setprod R R) z0 b) z HzU0).
We prove the intermediate claim HexD: ∃x0 : set, z = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1.
An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzD).
Apply HexD to the current goal.
Let x0 be given.
Assume Hx0pack.
Apply Hx0pack to the current goal.
Assume HcoreD Hx0lt1.
Apply HcoreD to the current goal.
Assume HzEq Hx0pos.
We prove the intermediate claim Hbltz: order_rel (setprod R R) b z.
rewrite the current goal using HzEq (from left to right).
Apply (order_rel_setprod_R_R_intro 0 (eps_ 1) x0 (eps_ 1)) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hx0pos.
We prove the intermediate claim HbR: b ∈ 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) b (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 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 (SepE1 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzD)).
We prove the intermediate claim Hbb: order_rel (setprod R R) b b.
An exact proof term for the current goal is (order_rel_trans (setprod R R) b z b simply_ordered_set_setprod_R_R HbR HzRR HbR Hbltz Hzltb).
An exact proof term for the current goal is ((order_rel_irref (setprod R R) b) Hbb).
We prove the intermediate claim HcapEq: U0 ∩ ordsq_D = Empty.
An exact proof term for the current goal is (Empty_Subq_eq (U0 ∩ ordsq_D) Hsub).
An exact proof term for the current goal is ((Hcond U0 HU0top HpU0) HcapEq).
Assume Hxn0: ¬ (x = 0).
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 Hn1ltx: ¬ (Rlt 1 x).
An exact proof term for the current goal is (andER (¬ (Rlt x 0)) (¬ (Rlt 1 x)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) x HxU)).
We prove the intermediate claim Hxpos: Rlt 0 x.
Apply (SNoLt_trichotomy_or_impred x 0 HxS SNo_0 (Rlt 0 x)) 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.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxn0 Hxeq0).
Assume H0ltx: 0 < x.
An exact proof term for the current goal is (RltI 0 x real_0 HxR H0ltx).
We prove the intermediate claim Hxlt1: Rlt x 1.
Apply (SNoLt_trichotomy_or_impred 1 x SNo_1 HxS (Rlt x 1)) to the current goal.
Assume H1ltx: 1 < x.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hn1ltx (RltI 1 x real_1 HxR H1ltx)).
Assume H1eqx: 1 = x.
Apply FalseE to the current goal.
We prove the intermediate claim Hxeq1: x = 1.
rewrite the current goal using H1eqx (from right to left) at position 1.
Use reflexivity.
An exact proof term for the current goal is (Hxn1 Hxeq1).
Assume Hxlt1S: x < 1.
An exact proof term for the current goal is (RltI x 1 HxR real_1 Hxlt1S).
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 x to witness the existential quantifier.
We will prove p = (x,0) ∧ Rlt 0 x ∧ Rlt x 1.
Apply andI to the current goal.
We will prove p = (x,0) ∧ Rlt 0 x.
Apply andI to the current goal.
rewrite the current goal using HpEta (from left to right) at position 1.
rewrite the current goal using Hy0 (from left to right) at position 1.
Use reflexivity.
An exact proof term for the current goal is Hxpos.
An exact proof term for the current goal is Hxlt1.
We prove the intermediate claim HdefDcl: ordsq_D_closure = ((ordsq_D ∪ ordsq_C) ∪ ordsq_top_edge_lt1) ∪ {ordsq_p10}.
Use reflexivity.
rewrite the current goal using HdefDcl (from left to right).
Apply binunionI1 to the current goal.
Apply binunionI1 to the current goal.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is HpC.
Assume Hyn0: ¬ (y = 0).
Apply (xm (y = 1)) to the current goal.
Assume Hy1: y = 1.
Apply (xm (x = 1)) to the current goal.
Assume Hx1: x = 1.
Apply FalseE to the current goal.
Set a to be the term (1,0).
Set U0 to be the term {z ∈ ordered_square|order_rel (setprod R R) a z}.
We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 ordered_square.
An exact proof term for the current goal is (Sep_In_Power ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0)).
Set Bint to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}}.
Set Blow to be the term {I ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}}.
Set Bup to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}}.
We prove the intermediate claim HU0basis: U0 ∈ ordered_square_order_basis.
We prove the intermediate claim HdefB: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).
Use reflexivity.
rewrite the current goal using HdefB (from left to right).
Apply binunionI2 to the current goal.
Apply (SepI (𝒫 ordered_square) (λI0 : set ⇒ ∃a0 ∈ ordered_square, I0 = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}) U0 HU0Pow) to the current goal.
We use a to witness the existential quantifier.
We will prove a ∈ ordered_square ∧ U0 = {x0 ∈ ordered_square|order_rel (setprod R R) a x0}.
Apply andI to the current goal.
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).
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 Hap: order_rel (setprod R R) a p.
rewrite the current goal using HpEta (from left to right) at position 1.
rewrite the current goal using Hx1 (from left to right) at position 1.
rewrite the current goal using Hy1 (from left to right) at position 1.
Apply (order_rel_setprod_R_R_intro 1 0 1 1) to the current goal.
Apply orIR to the current goal.
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 (λz0 : set ⇒ order_rel (setprod R R) a z0) p HpSq) to the current goal.
An exact proof term for the current goal is Hap.
We prove the intermediate claim Hsub: U0 ∩ ordsq_D ⊆ Empty.
Let z be given.
Assume Hz: z ∈ U0 ∩ ordsq_D.
We will prove z ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HzU0: z ∈ U0.
An exact proof term for the current goal is (binintersectE1 U0 ordsq_D z Hz).
We prove the intermediate claim HzD: z ∈ ordsq_D.
An exact proof term for the current goal is (binintersectE2 U0 ordsq_D z Hz).
We prove the intermediate claim Ha_lt_z: order_rel (setprod R R) a z.
An exact proof term for the current goal is (SepE2 ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0) z HzU0).
We prove the intermediate claim HexD: ∃x0 : set, z = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1.
An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzD).
Apply HexD to the current goal.
Let x0 be given.
Assume Hx0pack.
Apply Hx0pack to the current goal.
Assume HcoreD Hx0lt1.
Apply HcoreD to the current goal.
Assume HzEq Hx0pos.
We prove the intermediate claim Hz_lt_a: order_rel (setprod R R) z a.
rewrite the current goal using HzEq (from left to right).
Apply (order_rel_setprod_R_R_intro x0 (eps_ 1) 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 HaRR: a ∈ 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) a (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 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 (SepE1 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzD)).
We prove the intermediate claim Haa: order_rel (setprod R R) a a.
An exact proof term for the current goal is (order_rel_trans (setprod R R) a z a simply_ordered_set_setprod_R_R HaRR HzRR HaRR Ha_lt_z Hz_lt_a).
An exact proof term for the current goal is ((order_rel_irref (setprod R R) a) Haa).
We prove the intermediate claim HcapEq: U0 ∩ ordsq_D = Empty.
An exact proof term for the current goal is (Empty_Subq_eq (U0 ∩ ordsq_D) Hsub).
An exact proof term for the current goal is ((Hcond U0 HU0top HpU0) HcapEq).
Assume Hxn1: ¬ (x = 1).
We prove the intermediate claim Hn1ltx: ¬ (Rlt 1 x).
An exact proof term for the current goal is (andER (¬ (Rlt x 0)) (¬ (Rlt 1 x)) (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) x HxU)).
We prove the intermediate claim Hxlt1: Rlt x 1.
Apply (SNoLt_trichotomy_or_impred 1 x SNo_1 HxS (Rlt x 1)) to the current goal.
Assume H1ltx: 1 < x.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hn1ltx (RltI 1 x real_1 HxR H1ltx)).
Assume H1eqx: 1 = x.
Apply FalseE to the current goal.
We prove the intermediate claim Hxeq1: x = 1.
rewrite the current goal using H1eqx (from right to left) at position 1.
Use reflexivity.
An exact proof term for the current goal is (Hxn1 Hxeq1).
Assume Hxlt1S: x < 1.
An exact proof term for the current goal is (RltI x 1 HxR real_1 Hxlt1S).
We prove the intermediate claim HpTop: p ∈ ordsq_top_edge_lt1.
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 x to witness the existential quantifier.
We will prove (p = (x,1) ∧ x ∈ unit_interval) ∧ Rlt x 1.
Apply andI to the current goal.
We will prove p = (x,1) ∧ x ∈ unit_interval.
Apply andI to the current goal.
rewrite the current goal using HpEta (from left to right) at position 1.
rewrite the current goal using Hy1 (from left to right) at position 1.
Use reflexivity.
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is Hxlt1.
We prove the intermediate claim HdefDcl: ordsq_D_closure = ((ordsq_D ∪ ordsq_C) ∪ ordsq_top_edge_lt1) ∪ {ordsq_p10}.
Use reflexivity.
rewrite the current goal using HdefDcl (from left to right).
Apply binunionI1 to the current goal.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is HpTop.
Assume Hyn1: ¬ (y = 1).
Apply FalseE to the current goal.
Apply (xm (x = 0)) to the current goal.
Assume Hx0: x = 0.
Set a to be the term (0,0).
Set b to be the term (0,1).
Set U0 to be the term {z ∈ ordered_square|order_rel (setprod R R) a z ∧ order_rel (setprod R R) z b}.
We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 ordered_square.
An exact proof term for the current goal is (Sep_In_Power ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b)).
Set Bint to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}}.
Set Blow to be the term {I ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}}.
Set Bup to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}}.
We prove the intermediate claim HU0basis: U0 ∈ ordered_square_order_basis.
We prove the intermediate claim HdefB: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).
Use reflexivity.
rewrite the current goal using HdefB (from left to right).
Apply binunionI1 to the current goal.
Apply binunionI1 to the current goal.
Apply (SepI (𝒫 ordered_square) (λI0 : set ⇒ ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I0 = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}) U0 HU0Pow) to the current goal.
We use a to witness the existential quantifier.
We will prove a ∈ ordered_square ∧ ∃b0 ∈ ordered_square, U0 = {x0 ∈ ordered_square|order_rel (setprod R R) a x0 ∧ order_rel (setprod R R) x0 b0}.
Apply andI to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval 0 0 zero_in_unit_interval zero_in_unit_interval).
We use b to witness the existential quantifier.
We will prove b ∈ ordered_square ∧ U0 = {x0 ∈ ordered_square|order_rel (setprod R R) a x0 ∧ order_rel (setprod R R) x0 b}.
Apply andI to the current goal.
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).
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 Hynlt0: ¬ (Rlt y 0).
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)).
We prove the intermediate claim Hypos: Rlt 0 y.
Apply (SNoLt_trichotomy_or_impred y 0 HyS SNo_0 (Rlt 0 y)) to the current goal.
Assume Hylt0: y < 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hynlt0 (RltI y 0 HyR real_0 Hylt0)).
Assume Hyeq0: y = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hyn0 Hyeq0).
Assume H0lty: 0 < y.
An exact proof term for the current goal is (RltI 0 y real_0 HyR H0lty).
We prove the intermediate claim Hnot1lty: ¬ (Rlt 1 y).
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)).
We prove the intermediate claim Hylt1: Rlt y 1.
Apply (SNoLt_trichotomy_or_impred 1 y SNo_1 HyS (Rlt y 1)) to the current goal.
Assume H1ltyS: 1 < y.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnot1lty (RltI 1 y real_1 HyR H1ltyS)).
Assume H1eqy: 1 = y.
Apply FalseE to the current goal.
We prove the intermediate claim Hyeq1: y = 1.
rewrite the current goal using H1eqy (from right to left) at position 1.
Use reflexivity.
An exact proof term for the current goal is (Hyn1 Hyeq1).
Assume Hylt1S: y < 1.
An exact proof term for the current goal is (RltI y 1 HyR real_1 Hylt1S).
We prove the intermediate claim Hap: order_rel (setprod R R) a p.
rewrite the current goal using HpEta (from left to right) at position 1.
rewrite the current goal using Hx0 (from left to right) at position 1.
Apply (order_rel_setprod_R_R_intro 0 0 0 y) to the current goal.
Apply orIR to the current goal.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is Hypos.
We prove the intermediate claim Hpb: order_rel (setprod R R) p b.
rewrite the current goal using HpEta (from left to right) at position 1.
rewrite the current goal using Hx0 (from left to right) at position 1.
Apply (order_rel_setprod_R_R_intro 0 y 0 1) to the current goal.
Apply orIR to the current goal.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is Hylt1.
We prove the intermediate claim HpU0: p ∈ U0.
Apply (SepI ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b) p HpSq) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hap.
An exact proof term for the current goal is Hpb.
We prove the intermediate claim Hsub: U0 ∩ ordsq_D ⊆ Empty.
Let z be given.
Assume Hz: z ∈ U0 ∩ ordsq_D.
We will prove z ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HzU0: z ∈ U0.
An exact proof term for the current goal is (binintersectE1 U0 ordsq_D z Hz).
We prove the intermediate claim HzD: z ∈ ordsq_D.
An exact proof term for the current goal is (binintersectE2 U0 ordsq_D z Hz).
We prove the intermediate claim HzU0core: 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 (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b) z HzU0).
We prove the intermediate claim Hz_lt_b: order_rel (setprod R R) z b.
An exact proof term for the current goal is (andER (order_rel (setprod R R) a z) (order_rel (setprod R R) z b) HzU0core).
We prove the intermediate claim HexD: ∃x0 : set, z = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1.
An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzD).
Apply HexD to the current goal.
Let x0 be given.
Assume Hx0pack.
Apply Hx0pack to the current goal.
Assume HcoreD Hx0lt1.
Apply HcoreD to the current goal.
Assume HzEq Hx0pos.
We prove the intermediate claim Hb_lt_z: order_rel (setprod R R) b z.
rewrite the current goal using HzEq (from left to right).
Apply (order_rel_setprod_R_R_intro 0 1 x0 (eps_ 1)) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hx0pos.
We prove the intermediate claim HbR: b ∈ 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) b (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 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 (SepE1 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzD)).
We prove the intermediate claim Hbb: order_rel (setprod R R) b b.
An exact proof term for the current goal is (order_rel_trans (setprod R R) b z b simply_ordered_set_setprod_R_R HbR HzRR HbR Hb_lt_z Hz_lt_b).
An exact proof term for the current goal is ((order_rel_irref (setprod R R) b) Hbb).
We prove the intermediate claim HcapEq: U0 ∩ ordsq_D = Empty.
An exact proof term for the current goal is (Empty_Subq_eq (U0 ∩ ordsq_D) Hsub).
An exact proof term for the current goal is ((Hcond U0 HU0top HpU0) HcapEq).
Assume Hxn0: ¬ (x = 0).
Apply (xm (x = 1)) to the current goal.
Assume Hx1: x = 1.
Apply FalseE to the current goal.
Set a to be the term (1,0).
Set U1 to be the term {z ∈ ordered_square|order_rel (setprod R R) a z}.
We prove the intermediate claim HU1Pow: U1 ∈ 𝒫 ordered_square.
An exact proof term for the current goal is (Sep_In_Power ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0)).
Set Bint to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}}.
Set Blow to be the term {I ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}}.
Set Bup to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}}.
We prove the intermediate claim HU1basis: U1 ∈ ordered_square_order_basis.
We prove the intermediate claim HdefB: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).
Use reflexivity.
rewrite the current goal using HdefB (from left to right).
Apply binunionI2 to the current goal.
Apply (SepI (𝒫 ordered_square) (λI0 : set ⇒ ∃a0 ∈ ordered_square, I0 = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}) U1 HU1Pow) to the current goal.
We use a to witness the existential quantifier.
We will prove a ∈ ordered_square ∧ U1 = {x0 ∈ ordered_square|order_rel (setprod R R) a x0}.
Apply andI to the current goal.
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).
Use reflexivity.
We prove the intermediate claim HU1top: U1 ∈ 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 U1 HU1Pow HU1basis).
We prove the intermediate claim Hynlt0: ¬ (Rlt y 0).
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)).
We prove the intermediate claim Hypos: Rlt 0 y.
Apply (SNoLt_trichotomy_or_impred y 0 HyS SNo_0 (Rlt 0 y)) to the current goal.
Assume Hylt0: y < 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hynlt0 (RltI y 0 HyR real_0 Hylt0)).
Assume Hyeq0: y = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hyn0 Hyeq0).
Assume H0lty: 0 < y.
An exact proof term for the current goal is (RltI 0 y real_0 HyR H0lty).
We prove the intermediate claim Hap: order_rel (setprod R R) a p.
rewrite the current goal using HpEta (from left to right) at position 1.
rewrite the current goal using Hx1 (from left to right) at position 1.
Apply (order_rel_setprod_R_R_intro 1 0 1 y) to the current goal.
Apply orIR to the current goal.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is Hypos.
We prove the intermediate claim HpU1: p ∈ U1.
Apply (SepI ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0) p HpSq) to the current goal.
An exact proof term for the current goal is Hap.
We prove the intermediate claim Hsub: U1 ∩ ordsq_D ⊆ Empty.
Let z be given.
Assume Hz: z ∈ U1 ∩ ordsq_D.
We will prove z ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HzU1: z ∈ U1.
An exact proof term for the current goal is (binintersectE1 U1 ordsq_D z Hz).
We prove the intermediate claim HzD: z ∈ ordsq_D.
An exact proof term for the current goal is (binintersectE2 U1 ordsq_D z Hz).
We prove the intermediate claim Ha_lt_z: order_rel (setprod R R) a z.
An exact proof term for the current goal is (SepE2 ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0) z HzU1).
We prove the intermediate claim HexD: ∃x0 : set, z = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1.
An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzD).
Apply HexD to the current goal.
Let x0 be given.
Assume Hx0pack.
Apply Hx0pack to the current goal.
Assume HcoreD Hx0lt1.
Apply HcoreD to the current goal.
Assume HzEq Hx0pos.
We prove the intermediate claim Hz_lt_a: order_rel (setprod R R) z a.
rewrite the current goal using HzEq (from left to right).
Apply (order_rel_setprod_R_R_intro x0 (eps_ 1) 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 HaRR: a ∈ 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) a (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 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 (SepE1 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzD)).
We prove the intermediate claim Haa: order_rel (setprod R R) a a.
An exact proof term for the current goal is (order_rel_trans (setprod R R) a z a simply_ordered_set_setprod_R_R HaRR HzRR HaRR Ha_lt_z Hz_lt_a).
An exact proof term for the current goal is ((order_rel_irref (setprod R R) a) Haa).
We prove the intermediate claim HcapEq: U1 ∩ ordsq_D = Empty.
An exact proof term for the current goal is (Empty_Subq_eq (U1 ∩ ordsq_D) Hsub).
An exact proof term for the current goal is ((Hcond U1 HU1top HpU1) HcapEq).
Assume Hxn1: ¬ (x = 1).
We prove the intermediate claim HepsR: (eps_ 1) ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R (eps_ 1) eps_1_in_unit_interval).
We prove the intermediate claim HepsS: SNo (eps_ 1).
An exact proof term for the current goal is (real_SNo (eps_ 1) HepsR).
We prove the intermediate claim Hynlt0: ¬ (Rlt y 0).
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)).
We prove the intermediate claim Hypos: Rlt 0 y.
Apply (SNoLt_trichotomy_or_impred y 0 HyS SNo_0 (Rlt 0 y)) to the current goal.
Assume Hylt0: y < 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hynlt0 (RltI y 0 HyR real_0 Hylt0)).
Assume Hyeq0: y = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hyn0 Hyeq0).
Assume H0lty: 0 < y.
An exact proof term for the current goal is (RltI 0 y real_0 HyR H0lty).
We prove the intermediate claim Hnot1lty: ¬ (Rlt 1 y).
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)).
We prove the intermediate claim Hylt1: Rlt y 1.
Apply (SNoLt_trichotomy_or_impred 1 y SNo_1 HyS (Rlt y 1)) to the current goal.
Assume H1ltyS: 1 < y.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnot1lty (RltI 1 y real_1 HyR H1ltyS)).
Assume H1eqy: 1 = y.
Apply FalseE to the current goal.
We prove the intermediate claim Hyeq1: y = 1.
rewrite the current goal using H1eqy (from right to left) at position 1.
Use reflexivity.
An exact proof term for the current goal is (Hyn1 Hyeq1).
Assume Hylt1S: y < 1.
An exact proof term for the current goal is (RltI y 1 HyR real_1 Hylt1S).
Apply (SNoLt_trichotomy_or_impred y (eps_ 1) HyS HepsS False) to the current goal.
Assume HyltEpsS: y < (eps_ 1).
We prove the intermediate claim HyltEps: Rlt y (eps_ 1).
An exact proof term for the current goal is (RltI y (eps_ 1) HyR HepsR HyltEpsS).
Set a to be the term (x,0).
Set b to be the term (x,eps_ 1).
Set U0 to be the term {z ∈ ordered_square|order_rel (setprod R R) a z ∧ order_rel (setprod R R) z b}.
We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 ordered_square.
An exact proof term for the current goal is (Sep_In_Power ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b)).
Set Bint to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}}.
Set Blow to be the term {I ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}}.
Set Bup to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}}.
We prove the intermediate claim HU0basis: U0 ∈ ordered_square_order_basis.
We prove the intermediate claim HdefB: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).
Use reflexivity.
rewrite the current goal using HdefB (from left to right).
Apply binunionI1 to the current goal.
Apply binunionI1 to the current goal.
Apply (SepI (𝒫 ordered_square) (λI0 : set ⇒ ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I0 = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}) U0 HU0Pow) to the current goal.
We use a to witness the existential quantifier.
We will prove a ∈ ordered_square ∧ ∃b0 ∈ ordered_square, U0 = {x0 ∈ ordered_square|order_rel (setprod R R) a x0 ∧ order_rel (setprod R R) x0 b0}.
Apply andI to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval x 0 HxU zero_in_unit_interval).
We use b to witness the existential quantifier.
We will prove b ∈ ordered_square ∧ U0 = {x0 ∈ ordered_square|order_rel (setprod R R) a x0 ∧ order_rel (setprod R R) x0 b}.
Apply andI to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval x (eps_ 1) HxU eps_1_in_unit_interval).
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 Hap: order_rel (setprod R R) a p.
We prove the intermediate claim HaDef: a = (x,0).
Use reflexivity.
rewrite the current goal using HaDef (from left to right) at position 1.
rewrite the current goal using HpEta (from left to right) at position 2.
An exact proof term for the current goal is (order_rel_setprod_R_R_same_first x 0 y Hypos).
We prove the intermediate claim Hpb: order_rel (setprod R R) p b.
We prove the intermediate claim HbDef: b = (x,eps_ 1).
Use reflexivity.
rewrite the current goal using HbDef (from left to right) at position 1.
rewrite the current goal using HpEta (from left to right) at position 1.
An exact proof term for the current goal is (order_rel_setprod_R_R_same_first x y (eps_ 1) HyltEps).
We prove the intermediate claim HpU0: p ∈ U0.
Apply (SepI ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b) p HpSq) to the current goal.
An exact proof term for the current goal is (andI (order_rel (setprod R R) a p) (order_rel (setprod R R) p b) Hap Hpb).
We prove the intermediate claim HcapEq: U0 ∩ ordsq_D = Empty.
We prove the intermediate claim Hsub: U0 ∩ ordsq_D ⊆ Empty.
Let z be given.
Assume Hz: z ∈ U0 ∩ ordsq_D.
We will prove z ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HzU0: z ∈ U0.
An exact proof term for the current goal is (binintersectE1 U0 ordsq_D z Hz).
We prove the intermediate claim HzD: z ∈ ordsq_D.
An exact proof term for the current goal is (binintersectE2 U0 ordsq_D z Hz).
We prove the intermediate claim HzSq: z ∈ ordered_square.
An exact proof term for the current goal is (SepE1 ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b) z HzU0).
Set z1 to be the term z 0.
Set z2 to be the term z 1.
We prove the intermediate claim HzEta: z = (z1,z2).
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval z HzSq).
We prove the intermediate claim HzU0core: 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 (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b) z HzU0).
We prove the intermediate claim Haz: order_rel (setprod R R) a z.
An exact proof term for the current goal is (andEL (order_rel (setprod R R) a z) (order_rel (setprod R R) z b) HzU0core).
We prove the intermediate claim Hzb: order_rel (setprod R R) z b.
An exact proof term for the current goal is (andER (order_rel (setprod R R) a z) (order_rel (setprod R R) z b) HzU0core).
We prove the intermediate claim HaDef: a = (x,0).
Use reflexivity.
We prove the intermediate claim HbDef: b = (x,eps_ 1).
Use reflexivity.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R x HxU).
We prove the intermediate claim Haz': order_rel (setprod R R) (x,0) (z1,z2).
rewrite the current goal using HaDef (from right to left) at position 1.
rewrite the current goal using HzEta (from right to left) at position 1.
An exact proof term for the current goal is Haz.
We prove the intermediate claim Hzb': order_rel (setprod R R) (z1,z2) (x,eps_ 1).
rewrite the current goal using HzEta (from right to left) at position 1.
rewrite the current goal using HbDef (from right to left) at position 1.
An exact proof term for the current goal is Hzb.
We prove the intermediate claim HazDisj: Rlt x z1 ∨ (x = z1 ∧ Rlt 0 z2).
An exact proof term for the current goal is (order_rel_setprod_R_R_disj x 0 z1 z2 Haz').
We prove the intermediate claim HzbDisj: Rlt z1 x ∨ (z1 = x ∧ Rlt z2 (eps_ 1)).
An exact proof term for the current goal is (order_rel_setprod_R_R_disj z1 z2 x (eps_ 1) Hzb').
We prove the intermediate claim Hxz1Eq: x = z1.
Apply HazDisj to the current goal.
Assume Hxltz1: Rlt x z1.
Apply FalseE to the current goal.
Apply HzbDisj to the current goal.
Assume Hz1ltx: Rlt z1 x.
An exact proof term for the current goal is ((not_Rlt_sym x z1 Hxltz1) Hz1ltx).
Assume Hz1EqAnd: z1 = x ∧ Rlt z2 (eps_ 1).
Apply Hz1EqAnd to the current goal.
Assume Hz1eqx Hz2ltEps.
Apply FalseE to the current goal.
We prove the intermediate claim Hxltx: Rlt x x.
rewrite the current goal using Hz1eqx (from right to left) at position 2.
An exact proof term for the current goal is Hxltz1.
An exact proof term for the current goal is ((not_Rlt_refl x HxR) Hxltx).
Assume HxEqAnd: x = z1 ∧ Rlt 0 z2.
Apply HxEqAnd to the current goal.
Assume Hxz1 Hz2pos.
An exact proof term for the current goal is Hxz1.
We prove the intermediate claim Hz1eqx: z1 = x.
rewrite the current goal using Hxz1Eq (from left to right).
Use reflexivity.
We prove the intermediate claim Hz2ltEps: Rlt z2 (eps_ 1).
Apply HzbDisj to the current goal.
Assume Hz1ltx: Rlt z1 x.
Apply FalseE to the current goal.
We prove the intermediate claim Hxltx: Rlt x x.
rewrite the current goal using Hz1eqx (from right to left) at position 1.
An exact proof term for the current goal is Hz1ltx.
An exact proof term for the current goal is ((not_Rlt_refl x HxR) Hxltx).
Assume Hz1EqAnd: z1 = x ∧ Rlt z2 (eps_ 1).
Apply Hz1EqAnd to the current goal.
Assume _ Hlt.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim HexD: ∃x0 : set, z = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1.
An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzD).
Apply HexD to the current goal.
Let x0 be given.
Assume Hx0pack.
Apply Hx0pack to the current goal.
Assume HcoreD Hx0lt1.
Apply HcoreD to the current goal.
Assume HzEqD Hx0pos.
We prove the intermediate claim HzcoordsD: z1 = x0 ∧ z2 = (eps_ 1).
We prove the intermediate claim Htmp: (z1,z2) = (x0,eps_ 1).
rewrite the current goal using HzEta (from right to left) at position 1.
An exact proof term for the current goal is HzEqD.
An exact proof term for the current goal is (tuple_eq_coords z1 z2 x0 (eps_ 1) Htmp).
We prove the intermediate claim Hz2EqEps: z2 = (eps_ 1).
An exact proof term for the current goal is (andER (z1 = x0) (z2 = (eps_ 1)) HzcoordsD).
We prove the intermediate claim HepsltEps: Rlt (eps_ 1) (eps_ 1).
rewrite the current goal using Hz2EqEps (from right to left) at position 1.
An exact proof term for the current goal is Hz2ltEps.
An exact proof term for the current goal is ((not_Rlt_refl (eps_ 1) HepsR) HepsltEps).
An exact proof term for the current goal is (Empty_Subq_eq (U0 ∩ ordsq_D) Hsub).
An exact proof term for the current goal is ((Hcond U0 HU0top HpU0) HcapEq).
Assume HyeqEps: y = (eps_ 1).
An exact proof term for the current goal is (HynEps HyeqEps).
Assume HepsltyS: (eps_ 1) < y.
We prove the intermediate claim Hepslty: Rlt (eps_ 1) y.
An exact proof term for the current goal is (RltI (eps_ 1) y HepsR HyR HepsltyS).
Set a to be the term (x,eps_ 1).
Set b to be the term (x,1).
Set U0 to be the term {z ∈ ordered_square|order_rel (setprod R R) a z ∧ order_rel (setprod R R) z b}.
We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 ordered_square.
An exact proof term for the current goal is (Sep_In_Power ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b)).
Set Bint to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}}.
Set Blow to be the term {I ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}}.
Set Bup to be the term {I ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}}.
We prove the intermediate claim HU0basis: U0 ∈ ordered_square_order_basis.
We prove the intermediate claim HdefB: ordered_square_order_basis = ((Bint ∪ Blow) ∪ Bup).
Use reflexivity.
rewrite the current goal using HdefB (from left to right).
Apply binunionI1 to the current goal.
Apply binunionI1 to the current goal.
Apply (SepI (𝒫 ordered_square) (λI0 : set ⇒ ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I0 = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}) U0 HU0Pow) to the current goal.
We use a to witness the existential quantifier.
We will prove a ∈ ordered_square ∧ ∃b0 ∈ ordered_square, U0 = {x0 ∈ ordered_square|order_rel (setprod R R) a x0 ∧ order_rel (setprod R R) x0 b0}.
Apply andI to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval x (eps_ 1) HxU eps_1_in_unit_interval).
We use b to witness the existential quantifier.
We will prove b ∈ ordered_square ∧ U0 = {x0 ∈ ordered_square|order_rel (setprod R R) a x0 ∧ order_rel (setprod R R) x0 b}.
Apply andI to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval x 1 HxU one_in_unit_interval).
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 Hap: order_rel (setprod R R) a p.
We prove the intermediate claim HaDef: a = (x,eps_ 1).
Use reflexivity.
rewrite the current goal using HaDef (from left to right) at position 1.
rewrite the current goal using HpEta (from left to right) at position 2.
An exact proof term for the current goal is (order_rel_setprod_R_R_same_first x (eps_ 1) y Hepslty).
We prove the intermediate claim Hpb: order_rel (setprod R R) p b.
We prove the intermediate claim HbDef: b = (x,1).
Use reflexivity.
rewrite the current goal using HbDef (from left to right) at position 1.
rewrite the current goal using HpEta (from left to right) at position 1.
An exact proof term for the current goal is (order_rel_setprod_R_R_same_first x y 1 Hylt1).
We prove the intermediate claim HpU0: p ∈ U0.
Apply (SepI ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b) p HpSq) to the current goal.
An exact proof term for the current goal is (andI (order_rel (setprod R R) a p) (order_rel (setprod R R) p b) Hap Hpb).
We prove the intermediate claim HcapEq: U0 ∩ ordsq_D = Empty.
We prove the intermediate claim Hsub: U0 ∩ ordsq_D ⊆ Empty.
Let z be given.
Assume Hz: z ∈ U0 ∩ ordsq_D.
We will prove z ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HzU0: z ∈ U0.
An exact proof term for the current goal is (binintersectE1 U0 ordsq_D z Hz).
We prove the intermediate claim HzD: z ∈ ordsq_D.
An exact proof term for the current goal is (binintersectE2 U0 ordsq_D z Hz).
We prove the intermediate claim HzSq: z ∈ ordered_square.
An exact proof term for the current goal is (SepE1 ordered_square (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b) z HzU0).
Set z1 to be the term z 0.
Set z2 to be the term z 1.
We prove the intermediate claim HzEta: z = (z1,z2).
An exact proof term for the current goal is (setprod_eta unit_interval unit_interval z HzSq).
We prove the intermediate claim HzU0core: 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 (λz0 : set ⇒ order_rel (setprod R R) a z0 ∧ order_rel (setprod R R) z0 b) z HzU0).
We prove the intermediate claim Haz: order_rel (setprod R R) a z.
An exact proof term for the current goal is (andEL (order_rel (setprod R R) a z) (order_rel (setprod R R) z b) HzU0core).
We prove the intermediate claim Hzb: order_rel (setprod R R) z b.
An exact proof term for the current goal is (andER (order_rel (setprod R R) a z) (order_rel (setprod R R) z b) HzU0core).
We prove the intermediate claim HaDef: a = (x,eps_ 1).
Use reflexivity.
We prove the intermediate claim HbDef: b = (x,1).
Use reflexivity.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R x HxU).
We prove the intermediate claim Haz': order_rel (setprod R R) (x,eps_ 1) (z1,z2).
rewrite the current goal using HaDef (from right to left) at position 1.
rewrite the current goal using HzEta (from right to left) at position 1.
An exact proof term for the current goal is Haz.
We prove the intermediate claim Hzb': order_rel (setprod R R) (z1,z2) (x,1).
rewrite the current goal using HzEta (from right to left) at position 1.
rewrite the current goal using HbDef (from right to left) at position 1.
An exact proof term for the current goal is Hzb.
We prove the intermediate claim HazDisj: Rlt x z1 ∨ (x = z1 ∧ Rlt (eps_ 1) z2).
An exact proof term for the current goal is (order_rel_setprod_R_R_disj x (eps_ 1) z1 z2 Haz').
We prove the intermediate claim HzbDisj: Rlt z1 x ∨ (z1 = x ∧ Rlt z2 1).
An exact proof term for the current goal is (order_rel_setprod_R_R_disj z1 z2 x 1 Hzb').
We prove the intermediate claim HexD: ∃x0 : set, z = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1.
An exact proof term for the current goal is (SepE2 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) z HzD).
Apply HexD to the current goal.
Let x0 be given.
Assume Hx0pack.
Apply Hx0pack to the current goal.
Assume HcoreD Hx0lt1.
Apply HcoreD to the current goal.
Assume HzEqD Hx0pos.
We prove the intermediate claim HzcoordsD: z1 = x0 ∧ z2 = (eps_ 1).
We prove the intermediate claim Htmp: (z1,z2) = (x0,eps_ 1).
rewrite the current goal using HzEta (from right to left) at position 1.
An exact proof term for the current goal is HzEqD.
An exact proof term for the current goal is (tuple_eq_coords z1 z2 x0 (eps_ 1) Htmp).
We prove the intermediate claim Hz2EqEps: z2 = (eps_ 1).
An exact proof term for the current goal is (andER (z1 = x0) (z2 = (eps_ 1)) HzcoordsD).
Apply HazDisj to the current goal.
Assume Hxltz1: Rlt x z1.
Apply FalseE to the current goal.
Apply HzbDisj to the current goal.
Assume Hz1ltx: Rlt z1 x.
An exact proof term for the current goal is ((not_Rlt_sym x z1 Hxltz1) Hz1ltx).
Assume Hz1EqAnd: z1 = x ∧ Rlt z2 1.
Apply Hz1EqAnd to the current goal.
Assume Hz1eqx Hz2lt1.
Apply FalseE to the current goal.
We prove the intermediate claim Hxltx: Rlt x x.
rewrite the current goal using Hz1eqx (from right to left) at position 2.
An exact proof term for the current goal is Hxltz1.
An exact proof term for the current goal is ((not_Rlt_refl x HxR) Hxltx).
Assume HxEqAnd: x = z1 ∧ Rlt (eps_ 1) z2.
Apply HxEqAnd to the current goal.
Assume Hxz1 Hepsltz2.
We prove the intermediate claim HepsltEps: Rlt (eps_ 1) (eps_ 1).
rewrite the current goal using Hz2EqEps (from right to left) at position 2.
An exact proof term for the current goal is Hepsltz2.
An exact proof term for the current goal is ((not_Rlt_refl (eps_ 1) HepsR) HepsltEps).
An exact proof term for the current goal is (Empty_Subq_eq (U0 ∩ ordsq_D) Hsub).
An exact proof term for the current goal is ((Hcond U0 HU0top HpU0) HcapEq).
Let p be given.
Assume Hp: p ∈ ordsq_D_closure.
We will prove p ∈ closure_of ordered_square ordered_square_topology ordsq_D.
Apply (binunionE ((ordsq_D ∪ ordsq_C) ∪ ordsq_top_edge_lt1) {ordsq_p10} p Hp) to the current goal.
Assume HpL1: p ∈ (ordsq_D ∪ ordsq_C) ∪ ordsq_top_edge_lt1.
Apply (binunionE (ordsq_D ∪ ordsq_C) ordsq_top_edge_lt1 p HpL1) to the current goal.
Assume HpL2: p ∈ ordsq_D ∪ ordsq_C.
Apply (binunionE ordsq_D ordsq_C p HpL2) to the current goal.
Assume HpD: p ∈ ordsq_D.
We prove the intermediate claim HpSq: p ∈ ordered_square.
An exact proof term for the current goal is (SepE1 ordered_square (λp0 : set ⇒ ∃x0 : set, p0 = (x0,eps_ 1) ∧ Rlt 0 x0 ∧ Rlt x0 1) p HpD).
We prove the intermediate claim Hdefcl: closure_of ordered_square ordered_square_topology ordsq_D = {x ∈ ordered_square|∀U : set, U ∈ ordered_square_topology → x ∈ U → U ∩ ordsq_D ≠ Empty}.
Use reflexivity.
rewrite the current goal using Hdefcl (from left to right).
Apply (SepI ordered_square (λx0 : set ⇒ ∀U : set, U ∈ ordered_square_topology → x0 ∈ U → U ∩ ordsq_D ≠ Empty) 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_D ≠ Empty.
We prove the intermediate claim HpUD: p ∈ U ∩ ordsq_D.
An exact proof term for the current goal is (binintersectI U ordsq_D p HpU HpD).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ ordsq_D) p HpUD).
Assume HpC: p ∈ ordsq_C.
An exact proof term for the current goal is (ex17_18_C_Sub_closure_D p HpC).
Assume HpTop: p ∈ ordsq_top_edge_lt1.
An exact proof term for the current goal is (ex17_18_top_edge_lt1_Sub_closure_D p HpTop).
Assume Hp10: p ∈ {ordsq_p10}.
We prove the intermediate claim HpEq: p = ordsq_p10.
An exact proof term for the current goal is (SingE ordsq_p10 p Hp10).
rewrite the current goal using HpEq (from left to right).
An exact proof term for the current goal is ex17_18_p10_in_closure_D.
∎