Let p be given.
Assume Hpcl: p ∈ closure_of ordered_square ordered_square_topology ordsq_A.
We will prove p ∈ ordsq_A ∪ {ordsq_p01}.
Set p01 to be the term ordsq_p01.
We prove the intermediate claim Hp01def: p01 = (0,1).
Use reflexivity.
We prove the intermediate claim Hp01Sq: p01 ∈ ordered_square.
rewrite the current goal using Hp01def (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval 0 1 zero_in_unit_interval one_in_unit_interval).
We prove the intermediate claim Hp01RR: p01 ∈ setprod R R.
An exact proof term for the current goal is ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) p01 Hp01Sq).
We prove the intermediate claim Hdefcl: closure_of ordered_square ordered_square_topology ordsq_A = {x ∈ ordered_square|∀U : set, U ∈ ordered_square_topology → x ∈ U → U ∩ ordsq_A ≠ Empty}.
Use reflexivity.
We prove the intermediate claim Hpcl': p ∈ {x ∈ ordered_square|∀U : set, U ∈ ordered_square_topology → x ∈ U → U ∩ ordsq_A ≠ Empty}.
rewrite the current goal using Hdefcl (from right to left).
An exact proof term for the current goal is Hpcl.
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_A ≠ Empty) p Hpcl').
We prove the intermediate claim Hcond: ∀U : set, U ∈ ordered_square_topology → p ∈ U → U ∩ ordsq_A ≠ 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_A ≠ Empty) p Hpcl').
We prove the intermediate claim HpRR: p ∈ 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) p HpSq).
Apply (order_rel_trichotomy_or_impred (setprod R R) p01 p simply_ordered_set_setprod_R_R Hp01RR HpRR (p ∈ ordsq_A ∪ {ordsq_p01})) to the current goal.
Assume Hp01p: order_rel (setprod R R) p01 p.
Apply binunionI1 to the current goal.
Set x to be the term p 0.
Set y to be the term p 1.
We prove the intermediate claim HpEq: 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 HxI: 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 HyI: 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 HxR: x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R x HxI).
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R y HyI).
We prove the intermediate claim HyProp: ¬ (Rlt y 0) ∧ ¬ (Rlt 1 y).
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z 0) ∧ ¬ (Rlt 1 z)) y HyI).
We prove the intermediate claim Hnot1y: ¬ (Rlt 1 y).
An exact proof term for the current goal is (andER (¬ (Rlt y 0)) (¬ (Rlt 1 y)) HyProp).
We prove the intermediate claim Hp01p': order_rel (setprod R R) (0,1) (x,y).
rewrite the current goal using Hp01def (from right to left).
rewrite the current goal using HpEq (from right to left).
An exact proof term for the current goal is Hp01p.
We prove the intermediate claim Hex: ∃c1 c2 d1 d2 : set, (0,1) = (c1,c2) ∧ (x,y) = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).
An exact proof term for the current goal is (order_rel_setprod_R_R_unfold (0,1) (x,y) Hp01p').
We prove the intermediate claim Hxpos: Rlt 0 x.
Apply Hex to the current goal.
Let c1 be given.
Assume Hc1.
Apply Hc1 to the current goal.
Let c2 be given.
Assume Hc2.
Apply Hc2 to the current goal.
Let d1 be given.
Assume Hd1.
Apply Hd1 to the current goal.
Let d2 be given.
Assume Hcore.
Apply Hcore to the current goal.
Assume Hpair Hdisj.
Apply Hdisj to the current goal.
Assume Hlt: Rlt c1 d1.
We prove the intermediate claim Heq01: (0,1) = (c1,c2).
An exact proof term for the current goal is (andEL ((0,1) = (c1,c2)) ((x,y) = (d1,d2)) Hpair).
We prove the intermediate claim Heqp: (x,y) = (d1,d2).
An exact proof term for the current goal is (andER ((0,1) = (c1,c2)) ((x,y) = (d1,d2)) Hpair).
We prove the intermediate claim Hc1eq0: 0 = c1.
We prove the intermediate claim Htmp0: (0,1) 0 = (c1,c2) 0.
rewrite the current goal using Heq01 (from left to right).
Use reflexivity.
We prove the intermediate claim Htmp1: 0 = c1.
rewrite the current goal using (tuple_2_0_eq 0 1) (from right to left).
rewrite the current goal using (tuple_2_0_eq c1 c2) (from right to left).
An exact proof term for the current goal is Htmp0.
An exact proof term for the current goal is Htmp1.
We prove the intermediate claim Hd1eqx: x = d1.
We prove the intermediate claim Htmp0: (x,y) 0 = (d1,d2) 0.
rewrite the current goal using Heqp (from left to right).
Use reflexivity.
We prove the intermediate claim Htmp1: x = d1.
rewrite the current goal using (tuple_2_0_eq x y) (from right to left).
rewrite the current goal using (tuple_2_0_eq d1 d2) (from right to left).
An exact proof term for the current goal is Htmp0.
An exact proof term for the current goal is Htmp1.
rewrite the current goal using Hd1eqx (from left to right).
rewrite the current goal using Hc1eq0 (from left to right).
An exact proof term for the current goal is Hlt.
Assume Heq2: c1 = d1 ∧ Rlt c2 d2.
Apply FalseE to the current goal.
We prove the intermediate claim Heq01: (0,1) = (c1,c2).
An exact proof term for the current goal is (andEL ((0,1) = (c1,c2)) ((x,y) = (d1,d2)) Hpair).
We prove the intermediate claim Heqp: (x,y) = (d1,d2).
An exact proof term for the current goal is (andER ((0,1) = (c1,c2)) ((x,y) = (d1,d2)) Hpair).
We prove the intermediate claim Hc2eq1: c2 = 1.
We prove the intermediate claim Htmp0: (0,1) 1 = (c1,c2) 1.
rewrite the current goal using Heq01 (from left to right).
Use reflexivity.
We prove the intermediate claim Htmp1: 1 = c2.
rewrite the current goal using (tuple_2_1_eq 0 1) (from right to left).
rewrite the current goal using (tuple_2_1_eq c1 c2) (from right to left).
An exact proof term for the current goal is Htmp0.
rewrite the current goal using Htmp1 (from right to left).
Use reflexivity.
We prove the intermediate claim Hd2eqy: y = d2.
We prove the intermediate claim Htmp0: (x,y) 1 = (d1,d2) 1.
rewrite the current goal using Heqp (from left to right).
Use reflexivity.
We prove the intermediate claim Htmp1: y = d2.
rewrite the current goal using (tuple_2_1_eq x y) (from right to left).
rewrite the current goal using (tuple_2_1_eq d1 d2) (from right to left).
An exact proof term for the current goal is Htmp0.
An exact proof term for the current goal is Htmp1.
We prove the intermediate claim H1lty: Rlt 1 y.
We prove the intermediate claim Hlt12: Rlt c2 d2.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Heq2).
rewrite the current goal using Hd2eqy (from left to right).
rewrite the current goal using Hc2eq1 (from right to left).
An exact proof term for the current goal is Hlt12.
An exact proof term for the current goal is (Hnot1y H1lty).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
Apply (SNoLt_trichotomy_or_impred y 0 HyS SNo_0 (p ∈ ordsq_A)) to the current goal.
Assume Hylt0: y < 0.
Apply FalseE to the current goal.
We prove the intermediate claim Hnoty0: ¬ (Rlt y 0).
An exact proof term for the current goal is (andEL (¬ (Rlt y 0)) (¬ (Rlt 1 y)) HyProp).
We prove the intermediate claim Hyl0R: 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 (Hnoty0 Hyl0R).
Assume Hy0: y = 0.
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
Apply (xm (x ∈ K_set)) to the current goal.
Assume HxK: x ∈ K_set.
We prove the intermediate claim Hexn: ∃n ∈ ω ∖ {0}, x = inv_nat n.
An exact proof term for the current goal is (ReplE (ω ∖ {0}) (λn0 : set ⇒ inv_nat n0) x HxK).
Apply Hexn to the current goal.
Let n be given.
Assume Hnpack.
Apply Hnpack to the current goal.
Assume HnIn Hxeq.
We prove the intermediate claim Hpeq: p = (inv_nat n,0).
rewrite the current goal using HpEq (from left to right).
rewrite the current goal using Hxeq (from left to right).
rewrite the current goal using Hy0 (from left to right).
Use reflexivity.
rewrite the current goal using Hpeq (from left to right).
An exact proof term for the current goal is (ReplI (ω ∖ {0}) (λm0 : set ⇒ (inv_nat m0,0)) n HnIn).
Assume HxNotK: ¬ (x ∈ K_set).
Apply FalseE to the current goal.
We prove the intermediate claim H0ltx: 0 < x.
An exact proof term for the current goal is (RltE_lt 0 x Hxpos).
We prove the intermediate claim HexU: ∃U : set, U ∈ R_standard_topology ∧ x ∈ U ∧ U ∩ K_set = Empty.
An exact proof term for the current goal is (standard_open_neighborhood_disjoint_from_K_set_pos x HxR H0ltx HxNotK).
Apply HexU to the current goal.
Let U0 be given.
Assume HUpack.
We prove the intermediate claim Hcore: U0 ∈ R_standard_topology ∧ x ∈ U0.
An exact proof term for the current goal is (andEL (U0 ∈ R_standard_topology ∧ x ∈ U0) (U0 ∩ K_set = Empty) HUpack).
We prove the intermediate claim HU0Kempty: U0 ∩ K_set = Empty.
An exact proof term for the current goal is (andER (U0 ∈ R_standard_topology ∧ x ∈ U0) (U0 ∩ K_set = Empty) HUpack).
We prove the intermediate claim HU0open: U0 ∈ R_standard_topology.
An exact proof term for the current goal is (andEL (U0 ∈ R_standard_topology) (x ∈ U0) Hcore).
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (andER (U0 ∈ R_standard_topology) (x ∈ U0) Hcore).
We prove the intermediate claim Hexab: ∃a b : set, a ∈ R ∧ b ∈ R ∧ x ∈ open_interval a b ∧ open_interval a b ⊆ U0 ∧ Rlt a x ∧ Rlt x b.
An exact proof term for the current goal is (R_standard_open_refine_interval U0 x HU0open HxU0).
Apply Hexab to the current goal.
Let a be given.
Assume Hapak.
Apply Hapak to the current goal.
Let b be given.
Assume Habpack.
Apply Habpack to the current goal.
Assume Hab1 Hxltb.
Apply Hab1 to the current goal.
Assume Hab2 Haltx.
Apply Hab2 to the current goal.
Assume Hab3 HabSubU0.
Apply Hab3 to the current goal.
Assume HabR HxInt.
Apply HabR to the current goal.
Assume HaR HbR.
We prove the intermediate claim HabIntKempty: open_interval a b ∩ K_set = Empty.
Apply (Empty_Subq_eq (open_interval a b ∩ K_set)) to the current goal.
Let z be given.
Assume Hz: z ∈ open_interval a b ∩ K_set.
Apply FalseE to the current goal.
We prove the intermediate claim HzInt: z ∈ open_interval a b.
An exact proof term for the current goal is (binintersectE1 (open_interval a b) K_set z Hz).
We prove the intermediate claim HzK: z ∈ K_set.
An exact proof term for the current goal is (binintersectE2 (open_interval a b) K_set z Hz).
We prove the intermediate claim HzU0: z ∈ U0.
An exact proof term for the current goal is (HabSubU0 z HzInt).
We prove the intermediate claim HzU0K: z ∈ U0 ∩ K_set.
An exact proof term for the current goal is (binintersectI U0 K_set z HzU0 HzK).
We prove the intermediate claim HzEmpty: z ∈ Empty.
rewrite the current goal using HU0Kempty (from right to left).
An exact proof term for the current goal is HzU0K.
An exact proof term for the current goal is (EmptyE z HzEmpty).
We prove the intermediate claim HinvNotInt: ∀n : set, n ∈ ω ∖ {0} → ¬ (inv_nat n ∈ open_interval a b).
Let n be given.
Assume HnIn: n ∈ ω ∖ {0}.
An exact proof term for the current goal is (inv_nat_not_in_open_interval_of_empty_cap_K_set a b HabIntKempty n HnIn).
We prove the intermediate claim HxProp2: ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x).
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) x HxI).
We prove the intermediate claim Hnot1x: ¬ (Rlt 1 x).
An exact proof term for the current goal is (andER (¬ (Rlt x 0)) (¬ (Rlt 1 x)) HxProp2).
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 Hexq1: ∃q1 : set, q1 ∈ rational_numbers ∧ Rlt a q1 ∧ Rlt q1 x ∧ q1 ∈ unit_interval.
Apply (SNoLt_trichotomy_or_impred a 0 HaS SNo_0 (∃q1 : set, q1 ∈ rational_numbers ∧ Rlt a q1 ∧ Rlt q1 x ∧ q1 ∈ unit_interval)) to the current goal.
Assume Halt0: a < 0.
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).
Apply (rational_dense_between_reals 0 x real_0 HxR Hxpos) to the current goal.
Let q1 be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q1 ∈ rational_numbers.
Assume Hqprop: Rlt 0 q1 ∧ Rlt q1 x.
We prove the intermediate claim H0ltq1: Rlt 0 q1.
An exact proof term for the current goal is (andEL (Rlt 0 q1) (Rlt q1 x) Hqprop).
We prove the intermediate claim Hq1ltx: Rlt q1 x.
An exact proof term for the current goal is (andER (Rlt 0 q1) (Rlt q1 x) Hqprop).
We prove the intermediate claim HaLtq1: Rlt a q1.
An exact proof term for the current goal is (Rlt_tra a 0 q1 Halt0R H0ltq1).
We prove the intermediate claim Hq1R: q1 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q1 HqQ).
We prove the intermediate claim Hnltq10: ¬ (Rlt q1 0).
An exact proof term for the current goal is (not_Rlt_sym 0 q1 H0ltq1).
We prove the intermediate claim Hnlt1q1: ¬ (Rlt 1 q1).
Assume H1ltq1: Rlt 1 q1.
We prove the intermediate claim H1ltx: Rlt 1 x.
An exact proof term for the current goal is (Rlt_tra 1 q1 x H1ltq1 Hq1ltx).
An exact proof term for the current goal is (Hnot1x H1ltx).
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 Hnltq10.
An exact proof term for the current goal is Hnlt1q1.
We use q1 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HqQ.
An exact proof term for the current goal is HaLtq1.
An exact proof term for the current goal is Hq1ltx.
An exact proof term for the current goal is Hq1U.
Assume Haeq0: a = 0.
Apply (rational_dense_between_reals 0 x real_0 HxR Hxpos) to the current goal.
Let q1 be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q1 ∈ rational_numbers.
Assume Hqprop: Rlt 0 q1 ∧ Rlt q1 x.
We prove the intermediate claim H0ltq1: Rlt 0 q1.
An exact proof term for the current goal is (andEL (Rlt 0 q1) (Rlt q1 x) Hqprop).
We prove the intermediate claim Hq1ltx: Rlt q1 x.
An exact proof term for the current goal is (andER (Rlt 0 q1) (Rlt q1 x) Hqprop).
We prove the intermediate claim HaLtq1: Rlt a q1.
rewrite the current goal using Haeq0 (from left to right).
An exact proof term for the current goal is H0ltq1.
We prove the intermediate claim Hq1R: q1 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q1 HqQ).
We prove the intermediate claim Hnltq10: ¬ (Rlt q1 0).
An exact proof term for the current goal is (not_Rlt_sym 0 q1 H0ltq1).
We prove the intermediate claim Hnlt1q1: ¬ (Rlt 1 q1).
Assume H1ltq1: Rlt 1 q1.
We prove the intermediate claim H1ltx: Rlt 1 x.
An exact proof term for the current goal is (Rlt_tra 1 q1 x H1ltq1 Hq1ltx).
An exact proof term for the current goal is (Hnot1x H1ltx).
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 Hnltq10.
An exact proof term for the current goal is Hnlt1q1.
We use q1 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HqQ.
An exact proof term for the current goal is HaLtq1.
An exact proof term for the current goal is Hq1ltx.
An exact proof term for the current goal is Hq1U.
Assume H0lta: 0 < a.
We prove the intermediate claim H0ltaR: Rlt 0 a.
An exact proof term for the current goal is (RltI 0 a real_0 HaR H0lta).
Apply (rational_dense_between_reals a x HaR HxR Haltx) to the current goal.
Let q1 be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q1 ∈ rational_numbers.
Assume Hqprop: Rlt a q1 ∧ Rlt q1 x.
We prove the intermediate claim HaLtq1: Rlt a q1.
An exact proof term for the current goal is (andEL (Rlt a q1) (Rlt q1 x) Hqprop).
We prove the intermediate claim Hq1ltx: Rlt q1 x.
An exact proof term for the current goal is (andER (Rlt a q1) (Rlt q1 x) Hqprop).
We prove the intermediate claim H0ltq1: Rlt 0 q1.
An exact proof term for the current goal is (Rlt_tra 0 a q1 H0ltaR HaLtq1).
We prove the intermediate claim Hq1R: q1 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q1 HqQ).
We prove the intermediate claim Hnltq10: ¬ (Rlt q1 0).
An exact proof term for the current goal is (not_Rlt_sym 0 q1 H0ltq1).
We prove the intermediate claim Hnlt1q1: ¬ (Rlt 1 q1).
Assume H1ltq1: Rlt 1 q1.
We prove the intermediate claim H1ltx: Rlt 1 x.
An exact proof term for the current goal is (Rlt_tra 1 q1 x H1ltq1 Hq1ltx).
An exact proof term for the current goal is (Hnot1x H1ltx).
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 Hnltq10.
An exact proof term for the current goal is Hnlt1q1.
We use q1 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HqQ.
An exact proof term for the current goal is HaLtq1.
An exact proof term for the current goal is Hq1ltx.
An exact proof term for the current goal is Hq1U.
Apply Hexq1 to the current goal.
Let q1 be given.
Assume Hq1pack.
Apply Hq1pack to the current goal.
Assume Hq1left Hq1U.
Apply Hq1left to the current goal.
Assume Hq1left2 Hq1ltx.
Apply Hq1left2 to the current goal.
Assume Hq1Q HaLtq1.
Set W to be the term {z ∈ ordered_square|order_rel (setprod R R) (q1,1) z ∧ order_rel (setprod R R) z (x,eps_ 1)}.
We prove the intermediate claim HWpow: W ∈ 𝒫 ordered_square.
An exact proof term for the current goal is (Sep_In_Power ordered_square (λz0 : set ⇒ order_rel (setprod R R) (q1,1) z0 ∧ order_rel (setprod R R) z0 (x,eps_ 1))).
We prove the intermediate claim Ha0Sq: (q1,1) ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval q1 1 Hq1U one_in_unit_interval).
We prove the intermediate claim Hb0Sq: (x,eps_ 1) ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval x (eps_ 1) HxI eps_1_in_unit_interval).
We prove the intermediate claim HWbas: W ∈ ordered_square_order_basis.
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 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) (λI : set ⇒ ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}) W HWpow) to the current goal.
We use (q1,1) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0Sq.
We use (x,eps_ 1) 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 HWtop: W ∈ 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 W HWpow HWbas).
We prove the intermediate claim HpW: p ∈ W.
Apply (SepI ordered_square (λz0 : set ⇒ order_rel (setprod R R) (q1,1) z0 ∧ order_rel (setprod R R) z0 (x,eps_ 1)) p HpSq) to the current goal.
We prove the intermediate claim Hleft: order_rel (setprod R R) (q1,1) p.
rewrite the current goal using HpEq (from left to right).
rewrite the current goal using Hy0 (from left to right).
Apply (order_rel_setprod_R_R_intro q1 1 x 0) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hq1ltx.
We prove the intermediate claim Hright: order_rel (setprod R R) p (x,eps_ 1).
rewrite the current goal using HpEq (from left to right) at position 1.
rewrite the current goal using Hy0 (from left to right) at position 1.
An exact proof term for the current goal is (order_rel_setprod_R_R_same_first x 0 (eps_ 1) eps_1_pos_R).
An exact proof term for the current goal is (andI (order_rel (setprod R R) (q1,1) p) (order_rel (setprod R R) p (x,eps_ 1)) Hleft Hright).
We prove the intermediate claim HWcapEq: W ∩ ordsq_A = Empty.
We prove the intermediate claim HWcapSub: W ∩ ordsq_A ⊆ Empty.
Let w be given.
Assume Hw: w ∈ W ∩ ordsq_A.
We will prove w ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (binintersectE1 W ordsq_A w Hw).
We prove the intermediate claim HwA: w ∈ ordsq_A.
An exact proof term for the current goal is (binintersectE2 W ordsq_A w Hw).
We prove the intermediate claim Hexn: ∃n ∈ ω ∖ {0}, w = (inv_nat n,0).
An exact proof term for the current goal is (ReplE (ω ∖ {0}) (λm0 : set ⇒ (inv_nat m0,0)) w HwA).
Apply Hexn to the current goal.
Let n be given.
Assume Hnpack.
Apply Hnpack to the current goal.
Assume HnIn Hweq.
We prove the intermediate claim HnOmega: n ∈ ω.
An exact proof term for the current goal is (andEL (n ∈ ω) (n ∉ {0}) (setminusE ω {0} n HnIn)).
We prove the intermediate claim HinvR: inv_nat n ∈ R.
An exact proof term for the current goal is (inv_nat_real n HnOmega).
We prove the intermediate claim Hord1: order_rel (setprod R R) (q1,1) (inv_nat n,0).
We prove the intermediate claim Htmp: order_rel (setprod R R) (q1,1) w.
An exact proof term for the current goal is (andEL (order_rel (setprod R R) (q1,1) w) (order_rel (setprod R R) w (x,eps_ 1)) (SepE2 ordered_square (λz0 : set ⇒ order_rel (setprod R R) (q1,1) z0 ∧ order_rel (setprod R R) z0 (x,eps_ 1)) w HwW)).
rewrite the current goal using Hweq (from right to left).
An exact proof term for the current goal is Htmp.
We prove the intermediate claim Hord2: order_rel (setprod R R) (inv_nat n,0) (x,eps_ 1).
We prove the intermediate claim Htmp: order_rel (setprod R R) w (x,eps_ 1).
An exact proof term for the current goal is (andER (order_rel (setprod R R) (q1,1) w) (order_rel (setprod R R) w (x,eps_ 1)) (SepE2 ordered_square (λz0 : set ⇒ order_rel (setprod R R) (q1,1) z0 ∧ order_rel (setprod R R) z0 (x,eps_ 1)) w HwW)).
rewrite the current goal using Hweq (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
We prove the intermediate claim Hex1: ∃a1 a2 b1 b2 : set, (q1,1) = (a1,a2) ∧ (inv_nat n,0) = (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 (q1,1) (inv_nat n,0) Hord1).
We prove the intermediate claim Hq1ltInv: Rlt q1 (inv_nat n).
Apply Hex1 to the current goal.
Let a1 be given.
Assume Ha1.
Apply Ha1 to the current goal.
Let a2 be given.
Assume Ha2.
Apply Ha2 to the current goal.
Let b1 be given.
Assume Hb1.
Apply Hb1 to the current goal.
Let b2 be given.
Assume Hcore.
Apply Hcore to the current goal.
Assume Hpair Hdisj.
We prove the intermediate claim Hpa: (q1,1) = (a1,a2).
An exact proof term for the current goal is (andEL ((q1,1) = (a1,a2)) ((inv_nat n,0) = (b1,b2)) Hpair).
We prove the intermediate claim Hpb: (inv_nat n,0) = (b1,b2).
An exact proof term for the current goal is (andER ((q1,1) = (a1,a2)) ((inv_nat n,0) = (b1,b2)) Hpair).
We prove the intermediate claim Ha1eq: q1 = a1.
rewrite the current goal using (tuple_2_0_eq q1 1) (from right to left).
rewrite the current goal using (tuple_2_0_eq a1 a2) (from right to left).
We prove the intermediate claim H0eq: (q1,1) 0 = (a1,a2) 0.
rewrite the current goal using Hpa (from left to right).
Use reflexivity.
An exact proof term for the current goal is H0eq.
We prove the intermediate claim Ha2eq: 1 = a2.
rewrite the current goal using (tuple_2_1_eq q1 1) (from right to left).
rewrite the current goal using (tuple_2_1_eq a1 a2) (from right to left).
We prove the intermediate claim H1eq: (q1,1) 1 = (a1,a2) 1.
rewrite the current goal using Hpa (from left to right).
Use reflexivity.
An exact proof term for the current goal is H1eq.
We prove the intermediate claim Hb1eq: inv_nat n = b1.
rewrite the current goal using (tuple_2_0_eq (inv_nat n) 0) (from right to left).
rewrite the current goal using (tuple_2_0_eq b1 b2) (from right to left).
We prove the intermediate claim H0eq: (inv_nat n,0) 0 = (b1,b2) 0.
rewrite the current goal using Hpb (from left to right).
Use reflexivity.
An exact proof term for the current goal is H0eq.
We prove the intermediate claim Hb2eq: 0 = b2.
rewrite the current goal using (tuple_2_1_eq (inv_nat n) 0) (from right to left).
rewrite the current goal using (tuple_2_1_eq b1 b2) (from right to left).
We prove the intermediate claim H1eq: (inv_nat n,0) 1 = (b1,b2) 1.
rewrite the current goal using Hpb (from left to right).
Use reflexivity.
An exact proof term for the current goal is H1eq.
We prove the intermediate claim Hdisj': Rlt q1 (inv_nat n) ∨ (q1 = inv_nat n ∧ Rlt 1 0).
rewrite the current goal using Ha1eq (from left to right).
rewrite the current goal using Hb1eq (from left to right).
rewrite the current goal using Ha2eq (from left to right).
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is Hdisj.
Apply Hdisj' to the current goal.
Assume Hlt.
An exact proof term for the current goal is Hlt.
Assume Hbad.
Apply FalseE to the current goal.
We prove the intermediate claim H10: Rlt 1 0.
An exact proof term for the current goal is (andER (q1 = inv_nat n) (Rlt 1 0) Hbad).
An exact proof term for the current goal is ((not_Rlt_sym 0 1 Rlt_0_1) H10).
We prove the intermediate claim Hex2: ∃a1 a2 b1 b2 : set, (inv_nat n,0) = (a1,a2) ∧ (x,eps_ 1) = (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 (inv_nat n,0) (x,eps_ 1) Hord2).
We prove the intermediate claim Hinvltx: Rlt (inv_nat n) x.
Apply Hex2 to the current goal.
Let a1 be given.
Assume Ha1.
Apply Ha1 to the current goal.
Let a2 be given.
Assume Ha2.
Apply Ha2 to the current goal.
Let b1 be given.
Assume Hb1.
Apply Hb1 to the current goal.
Let b2 be given.
Assume Hcore.
Apply Hcore to the current goal.
Assume Hpair Hdisj.
We prove the intermediate claim Hpa: (inv_nat n,0) = (a1,a2).
An exact proof term for the current goal is (andEL ((inv_nat n,0) = (a1,a2)) ((x,eps_ 1) = (b1,b2)) Hpair).
We prove the intermediate claim Hpb: (x,eps_ 1) = (b1,b2).
An exact proof term for the current goal is (andER ((inv_nat n,0) = (a1,a2)) ((x,eps_ 1) = (b1,b2)) Hpair).
We prove the intermediate claim Ha1eq: inv_nat n = a1.
rewrite the current goal using (tuple_2_0_eq (inv_nat n) 0) (from right to left).
rewrite the current goal using (tuple_2_0_eq a1 a2) (from right to left).
We prove the intermediate claim H0eq: (inv_nat n,0) 0 = (a1,a2) 0.
rewrite the current goal using Hpa (from left to right).
Use reflexivity.
An exact proof term for the current goal is H0eq.
We prove the intermediate claim Ha2eq: 0 = a2.
rewrite the current goal using (tuple_2_1_eq (inv_nat n) 0) (from right to left).
rewrite the current goal using (tuple_2_1_eq a1 a2) (from right to left).
We prove the intermediate claim H1eq: (inv_nat n,0) 1 = (a1,a2) 1.
rewrite the current goal using Hpa (from left to right).
Use reflexivity.
An exact proof term for the current goal is H1eq.
We prove the intermediate claim Hb1eq: x = b1.
rewrite the current goal using (tuple_2_0_eq x (eps_ 1)) (from right to left).
rewrite the current goal using (tuple_2_0_eq b1 b2) (from right to left).
We prove the intermediate claim H0eq: (x,eps_ 1) 0 = (b1,b2) 0.
rewrite the current goal using Hpb (from left to right).
Use reflexivity.
An exact proof term for the current goal is H0eq.
Apply Hdisj to the current goal.
Assume Hlt: Rlt a1 b1.
rewrite the current goal using Ha1eq (from left to right).
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is Hlt.
Assume Heq_and: a1 = b1 ∧ Rlt a2 b2.
Apply FalseE to the current goal.
We prove the intermediate claim Heq1: a1 = b1.
An exact proof term for the current goal is (andEL (a1 = b1) (Rlt a2 b2) Heq_and).
We prove the intermediate claim Heq: inv_nat n = x.
rewrite the current goal using Ha1eq (from left to right).
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is Heq1.
We prove the intermediate claim HxK: x ∈ K_set.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is (ReplI (ω ∖ {0}) (λt : set ⇒ inv_nat t) n HnIn).
An exact proof term for the current goal is (HxNotK HxK).
We prove the intermediate claim Hainv: Rlt a (inv_nat n).
An exact proof term for the current goal is (Rlt_tra a q1 (inv_nat n) HaLtq1 Hq1ltInv).
We prove the intermediate claim Hinvb: Rlt (inv_nat n) b.
An exact proof term for the current goal is (Rlt_tra (inv_nat n) x b Hinvltx Hxltb).
We prove the intermediate claim HinvInt: inv_nat n ∈ open_interval a b.
We prove the intermediate claim Hop_def: open_interval a b = {t ∈ R|Rlt a t ∧ Rlt t b}.
Use reflexivity.
rewrite the current goal using Hop_def (from left to right).
Apply (SepI R (λt : set ⇒ Rlt a t ∧ Rlt t b) (inv_nat n) HinvR) to the current goal.
An exact proof term for the current goal is (andI (Rlt a (inv_nat n)) (Rlt (inv_nat n) b) Hainv Hinvb).
An exact proof term for the current goal is ((HinvNotInt n HnIn) HinvInt).
An exact proof term for the current goal is (Empty_Subq_eq (W ∩ ordsq_A) HWcapSub).
An exact proof term for the current goal is ((Hcond W HWtop HpW) HWcapEq).
Assume H0lty: 0 < y.
Apply FalseE to the current goal.
We prove the intermediate claim H0ltyR: Rlt 0 y.
An exact proof term for the current goal is (RltI 0 y real_0 HyR H0lty).
Apply (SNoLt_trichotomy_or_impred y 1 HyS SNo_1 False) to the current goal.
Assume Hylt1: y < 1.
Apply (rational_dense_between_reals 0 y real_0 HyR H0ltyR) to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume Hqprop: Rlt 0 q ∧ Rlt q y.
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (andEL (Rlt 0 q) (Rlt q y) Hqprop).
We prove the intermediate claim Hqlty: Rlt q y.
An exact proof term for the current goal is (andER (Rlt 0 q) (Rlt q y) Hqprop).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim Hylt1R: Rlt y 1.
An exact proof term for the current goal is (RltI y 1 HyR real_1 Hylt1).
Apply (rational_dense_between_reals y 1 HyR real_1 Hylt1R) to the current goal.
Let y2 be given.
Assume Hy2pair.
Apply Hy2pair to the current goal.
Assume Hy2Q: y2 ∈ rational_numbers.
Assume Hy2prop: Rlt y y2 ∧ Rlt y2 1.
We prove the intermediate claim Hylt_y2: Rlt y y2.
An exact proof term for the current goal is (andEL (Rlt y y2) (Rlt y2 1) Hy2prop).
We prove the intermediate claim Hy2lt1: Rlt y2 1.
An exact proof term for the current goal is (andER (Rlt y y2) (Rlt y2 1) Hy2prop).
We prove the intermediate claim Hy2R: y2 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R y2 Hy2Q).
Set a0 to be the term (x,q).
Set b0 to be the term (x,y2).
We prove the intermediate claim Ha0Sq: a0 ∈ ordered_square.
We prove the intermediate claim Hsqdef: ordered_square = setprod unit_interval unit_interval.
Use reflexivity.
rewrite the current goal using Hsqdef (from left to right).
We prove the intermediate claim Ha0def: a0 = (x,q).
Use reflexivity.
rewrite the current goal using Ha0def (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval x q HxI (SepI R (λz : set ⇒ ¬ (Rlt z 0) ∧ ¬ (Rlt 1 z)) q HqR (andI (¬ (Rlt q 0)) (¬ (Rlt 1 q)) (not_Rlt_sym 0 q H0ltq) (not_Rlt_sym q 1 (Rlt_tra q y 1 Hqlty Hylt1R))))).
We prove the intermediate claim Hb0Sq: b0 ∈ ordered_square.
We prove the intermediate claim Hsqdef: ordered_square = setprod unit_interval unit_interval.
Use reflexivity.
rewrite the current goal using Hsqdef (from left to right).
We prove the intermediate claim Hb0def: b0 = (x,y2).
Use reflexivity.
rewrite the current goal using Hb0def (from left to right).
We prove the intermediate claim H0lty2: Rlt 0 y2.
An exact proof term for the current goal is (Rlt_tra 0 y y2 H0ltyR Hylt_y2).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval x y2 HxI (SepI R (λz : set ⇒ ¬ (Rlt z 0) ∧ ¬ (Rlt 1 z)) y2 Hy2R (andI (¬ (Rlt y2 0)) (¬ (Rlt 1 y2)) (not_Rlt_sym 0 y2 H0lty2) (not_Rlt_sym y2 1 Hy2lt1)))).
Set U to be the term {z ∈ ordered_square|order_rel (setprod R R) a0 z ∧ order_rel (setprod R R) z b0}.
We prove the intermediate claim HUpow: U ∈ 𝒫 ordered_square.
Apply (PowerI ordered_square U) to the current goal.
Let z be given.
Assume Hz: z ∈ U.
An exact proof term for the current goal is (SepE1 ordered_square (λz0 : set ⇒ order_rel (setprod R R) a0 z0 ∧ order_rel (setprod R R) z0 b0) z Hz).
We prove the intermediate claim HUbas: U ∈ ordered_square_order_basis.
Set Bint to be the term {J ∈ 𝒫 ordered_square|∃a1 ∈ ordered_square, ∃b1 ∈ ordered_square, J = {x0 ∈ ordered_square|order_rel (setprod R R) a1 x0 ∧ order_rel (setprod R R) x0 b1}}.
Set Blow to be the term {J ∈ 𝒫 ordered_square|∃b1 ∈ ordered_square, J = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b1}}.
Set Bup to be the term {J ∈ 𝒫 ordered_square|∃a1 ∈ ordered_square, J = {x0 ∈ ordered_square|order_rel (setprod R R) a1 x0}}.
We prove the intermediate claim HUinBint: U ∈ Bint.
Apply (SepI (𝒫 ordered_square) (λJ0 : set ⇒ ∃a1 ∈ ordered_square, ∃b1 ∈ ordered_square, J0 = {x0 ∈ ordered_square|order_rel (setprod R R) a1 x0 ∧ order_rel (setprod R R) x0 b1}) U HUpow) to the current goal.
We use a0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0Sq.
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 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.
An exact proof term for the current goal is HUinBint.
We prove the intermediate claim HUtop: U ∈ 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 U HUpow HUbas).
We prove the intermediate claim HpU: p ∈ U.
Apply (SepI ordered_square (λz0 : set ⇒ order_rel (setprod R R) a0 z0 ∧ order_rel (setprod R R) z0 b0) p) to the current goal.
An exact proof term for the current goal is HpSq.
We will prove order_rel (setprod R R) a0 p ∧ order_rel (setprod R R) p b0.
We prove the intermediate claim Ha0def: a0 = (x,q).
Use reflexivity.
We prove the intermediate claim Hb0def: b0 = (x,y2).
Use reflexivity.
We prove the intermediate claim Hleft: order_rel (setprod R R) a0 p.
rewrite the current goal using Ha0def (from left to right) at position 1.
rewrite the current goal using HpEq (from left to right) at position 2.
An exact proof term for the current goal is (order_rel_setprod_R_R_same_first x q y Hqlty).
We prove the intermediate claim Hright: order_rel (setprod R R) p b0.
rewrite the current goal using HpEq (from left to right) at position 1.
rewrite the current goal using Hb0def (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 y2 Hylt_y2).
An exact proof term for the current goal is (andI (order_rel (setprod R R) a0 p) (order_rel (setprod R R) p b0) Hleft Hright).
We prove the intermediate claim HcapEq: U ∩ ordsq_A = Empty.
Apply (Empty_Subq_eq (U ∩ ordsq_A)) to the current goal.
Let z be given.
Assume Hz: z ∈ U ∩ ordsq_A.
Apply FalseE to the current goal.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (binintersectE1 U ordsq_A z Hz).
We prove the intermediate claim HzA: z ∈ ordsq_A.
An exact proof term for the current goal is (binintersectE2 U ordsq_A z Hz).
Apply (ReplE_impred (ω ∖ {0}) (λn : set ⇒ (inv_nat n,0)) z HzA False) to the current goal.
Let n be given.
Assume HnIn: n ∈ ω ∖ {0}.
Assume HzEq: z = (inv_nat n,0).
We prove the intermediate claim HzRel: order_rel (setprod R R) a0 z ∧ order_rel (setprod R R) z b0.
An exact proof term for the current goal is (SepE2 ordered_square (λz0 : set ⇒ order_rel (setprod R R) a0 z0 ∧ order_rel (setprod R R) z0 b0) z HzU).
We prove the intermediate claim HzOrd1: order_rel (setprod R R) a0 z.
An exact proof term for the current goal is (andEL (order_rel (setprod R R) a0 z) (order_rel (setprod R R) z b0) HzRel).
We prove the intermediate claim HzOrd2: order_rel (setprod R R) z b0.
An exact proof term for the current goal is (andER (order_rel (setprod R R) a0 z) (order_rel (setprod R R) z b0) HzRel).
We prove the intermediate claim Ha0def: a0 = (x,q).
Use reflexivity.
We prove the intermediate claim Hb0def: b0 = (x,y2).
Use reflexivity.
We prove the intermediate claim HzOrd1': order_rel (setprod R R) (x,q) (inv_nat n,0).
rewrite the current goal using HzEq (from right to left).
rewrite the current goal using Ha0def (from right to left).
An exact proof term for the current goal is HzOrd1.
We prove the intermediate claim HzOrd2': order_rel (setprod R R) (inv_nat n,0) (x,y2).
rewrite the current goal using HzEq (from right to left).
rewrite the current goal using Hb0def (from right to left).
An exact proof term for the current goal is HzOrd2.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R x HxI).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (setminusE1 ω {0} n HnIn).
We prove the intermediate claim HinvR: inv_nat n ∈ R.
An exact proof term for the current goal is (inv_nat_real n HnO).
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim Hy2R: y2 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R y2 Hy2Q).
We prove the intermediate claim HxltInv: Rlt x (inv_nat n).
We prove the intermediate claim Hex1: ∃a1 a2 b1 b2 : set, (x,q) = (a1,a2) ∧ (inv_nat n,0) = (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 (x,q) (inv_nat n,0) HzOrd1').
Apply Hex1 to the current goal.
Let a1 be given.
Assume Ha1.
Apply Ha1 to the current goal.
Let a2 be given.
Assume Ha2.
Apply Ha2 to the current goal.
Let b1 be given.
Assume Hb1.
Apply Hb1 to the current goal.
Let b2 be given.
Assume Hpack1.
We prove the intermediate claim Hpair: (x,q) = (a1,a2) ∧ (inv_nat n,0) = (b1,b2).
An exact proof term for the current goal is (andEL ((x,q) = (a1,a2) ∧ (inv_nat n,0) = (b1,b2)) (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)) Hpack1).
We prove the intermediate claim Hdisj: Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2).
An exact proof term for the current goal is (andER ((x,q) = (a1,a2) ∧ (inv_nat n,0) = (b1,b2)) (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)) Hpack1).
We prove the intermediate claim HaPair: (x,q) = (a1,a2).
An exact proof term for the current goal is (andEL ((x,q) = (a1,a2)) ((inv_nat n,0) = (b1,b2)) Hpair).
We prove the intermediate claim HbPair: (inv_nat n,0) = (b1,b2).
An exact proof term for the current goal is (andER ((x,q) = (a1,a2)) ((inv_nat n,0) = (b1,b2)) Hpair).
We prove the intermediate claim HxEq: x = a1.
rewrite the current goal using (tuple_2_0_eq x q) (from right to left).
rewrite the current goal using (tuple_2_0_eq a1 a2) (from right to left).
We prove the intermediate claim H0eq: (x,q) 0 = (a1,a2) 0.
rewrite the current goal using HaPair (from left to right) at position 1.
Use reflexivity.
An exact proof term for the current goal is H0eq.
We prove the intermediate claim HqEq: q = a2.
rewrite the current goal using (tuple_2_1_eq x q) (from right to left).
rewrite the current goal using (tuple_2_1_eq a1 a2) (from right to left).
We prove the intermediate claim H1eq: (x,q) 1 = (a1,a2) 1.
rewrite the current goal using HaPair (from left to right) at position 1.
Use reflexivity.
An exact proof term for the current goal is H1eq.
We prove the intermediate claim Hb1Eq: inv_nat n = b1.
rewrite the current goal using (tuple_2_0_eq (inv_nat n) 0) (from right to left).
rewrite the current goal using (tuple_2_0_eq b1 b2) (from right to left).
We prove the intermediate claim H0eq: (inv_nat n,0) 0 = (b1,b2) 0.
rewrite the current goal using HbPair (from left to right) at position 1.
Use reflexivity.
An exact proof term for the current goal is H0eq.
We prove the intermediate claim Hb2Eq: 0 = b2.
rewrite the current goal using (tuple_2_1_eq (inv_nat n) 0) (from right to left).
rewrite the current goal using (tuple_2_1_eq b1 b2) (from right to left).
We prove the intermediate claim H1eq: (inv_nat n,0) 1 = (b1,b2) 1.
rewrite the current goal using HbPair (from left to right) at position 1.
Use reflexivity.
An exact proof term for the current goal is H1eq.
We prove the intermediate claim Hdisj': Rlt x (inv_nat n) ∨ (x = inv_nat n ∧ Rlt q 0).
rewrite the current goal using HxEq (from left to right).
rewrite the current goal using Hb1Eq (from left to right).
rewrite the current goal using HqEq (from left to right).
rewrite the current goal using Hb2Eq (from left to right).
An exact proof term for the current goal is Hdisj.
Apply Hdisj' to the current goal.
Assume Hxlt.
An exact proof term for the current goal is Hxlt.
Assume Hbad.
Apply FalseE to the current goal.
We prove the intermediate claim Hq0: Rlt q 0.
An exact proof term for the current goal is (andER (x = inv_nat n) (Rlt q 0) Hbad).
An exact proof term for the current goal is ((not_Rlt_sym 0 q H0ltq) Hq0).
We prove the intermediate claim Hex2: ∃a1 a2 b1 b2 : set, (inv_nat n,0) = (a1,a2) ∧ (x,y2) = (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 (inv_nat n,0) (x,y2) HzOrd2').
Apply Hex2 to the current goal.
Let a1 be given.
Assume Ha1.
Apply Ha1 to the current goal.
Let a2 be given.
Assume Ha2.
Apply Ha2 to the current goal.
Let b1 be given.
Assume Hb1.
Apply Hb1 to the current goal.
Let b2 be given.
Assume Hpack2.
We prove the intermediate claim Hpair2: (inv_nat n,0) = (a1,a2) ∧ (x,y2) = (b1,b2).
An exact proof term for the current goal is (andEL ((inv_nat n,0) = (a1,a2) ∧ (x,y2) = (b1,b2)) (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)) Hpack2).
We prove the intermediate claim Hdisj2: Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2).
An exact proof term for the current goal is (andER ((inv_nat n,0) = (a1,a2) ∧ (x,y2) = (b1,b2)) (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)) Hpack2).
We prove the intermediate claim HaPair2: (inv_nat n,0) = (a1,a2).
An exact proof term for the current goal is (andEL ((inv_nat n,0) = (a1,a2)) ((x,y2) = (b1,b2)) Hpair2).
We prove the intermediate claim HbPair2: (x,y2) = (b1,b2).
An exact proof term for the current goal is (andER ((inv_nat n,0) = (a1,a2)) ((x,y2) = (b1,b2)) Hpair2).
We prove the intermediate claim Ha1Eq: a1 = inv_nat n.
rewrite the current goal using (tuple_2_0_eq a1 a2) (from right to left).
rewrite the current goal using (tuple_2_0_eq (inv_nat n) 0) (from right to left).
We prove the intermediate claim H0eq: (a1,a2) 0 = (inv_nat n,0) 0.
rewrite the current goal using HaPair2 (from right to left) at position 1.
Use reflexivity.
An exact proof term for the current goal is H0eq.
We prove the intermediate claim Hb1Eq: b1 = x.
rewrite the current goal using (tuple_2_0_eq b1 b2) (from right to left).
rewrite the current goal using (tuple_2_0_eq x y2) (from right to left).
We prove the intermediate claim H0eq: (b1,b2) 0 = (x,y2) 0.
rewrite the current goal using HbPair2 (from right to left) at position 1.
Use reflexivity.
An exact proof term for the current goal is H0eq.
We prove the intermediate claim Ha2Eq: a2 = 0.
We prove the intermediate claim Htmp0: (inv_nat n,0) 1 = (a1,a2) 1.
rewrite the current goal using HaPair2 (from left to right).
Use reflexivity.
We prove the intermediate claim Htmp1: 0 = a2.
rewrite the current goal using (tuple_2_1_eq (inv_nat n) 0) (from right to left).
rewrite the current goal using (tuple_2_1_eq a1 a2) (from right to left).
An exact proof term for the current goal is Htmp0.
rewrite the current goal using Htmp1 (from right to left).
Use reflexivity.
We prove the intermediate claim Hb2Eq: b2 = y2.
rewrite the current goal using (tuple_2_1_eq b1 b2) (from right to left).
rewrite the current goal using (tuple_2_1_eq x y2) (from right to left).
We prove the intermediate claim H1eq: (b1,b2) 1 = (x,y2) 1.
rewrite the current goal using HbPair2 (from right to left) at position 1.
Use reflexivity.
An exact proof term for the current goal is H1eq.
We prove the intermediate claim H0lty2: Rlt 0 y2.
An exact proof term for the current goal is (Rlt_tra 0 y y2 H0ltyR Hylt_y2).
We prove the intermediate claim Hdisj2': Rlt (inv_nat n) x ∨ (inv_nat n = x ∧ Rlt 0 y2).
rewrite the current goal using Ha1Eq (from right to left) at position 1.
rewrite the current goal using Hb1Eq (from right to left) at position 1.
rewrite the current goal using Ha1Eq (from right to left) at position 1.
rewrite the current goal using Hb1Eq (from right to left) at position 1.
rewrite the current goal using Ha2Eq (from right to left) at position 1.
rewrite the current goal using Hb2Eq (from right to left) at position 1.
An exact proof term for the current goal is Hdisj2.
Apply Hdisj2' to the current goal.
Assume Hinvltx.
An exact proof term for the current goal is ((not_Rlt_sym (inv_nat n) x Hinvltx) HxltInv).
Assume Heq_and.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: inv_nat n = x.
An exact proof term for the current goal is (andEL (inv_nat n = x) (Rlt 0 y2) Heq_and).
We prove the intermediate claim Hxx: Rlt x x.
rewrite the current goal using Heq (from right to left) at position 2.
An exact proof term for the current goal is HxltInv.
An exact proof term for the current goal is (not_Rlt_refl x HxR Hxx).
An exact proof term for the current goal is ((Hcond U HUtop HpU) HcapEq).
Assume HyEq1: y = 1.
Apply FalseE to the current goal.
We prove the intermediate claim HpEq1: p = (x,1).
rewrite the current goal using HpEq (from left to right) at position 1.
rewrite the current goal using HyEq1 (from left to right) at position 1.
Use reflexivity.
Apply (xm (x = 1)) to the current goal.
Assume Hx1: x = 1.
Set U1 to be the term {z ∈ ordered_square|order_rel (setprod R R) (1,0) 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) (1,0) z0)).
Set Bint to be the term {J ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, J = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}}.
Set Blow to be the term {J ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, J = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}}.
Set Bup to be the term {J ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, J = {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) (λJ0 : set ⇒ ∃a0 ∈ ordered_square, J0 = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}) U1 HU1Pow) to the current goal.
We use (1,0) to witness the existential quantifier.
We will prove (1,0) ∈ ordered_square ∧ U1 = {x0 ∈ ordered_square|order_rel (setprod R R) (1,0) 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 HpU1: p ∈ U1.
Apply (SepI ordered_square (λz0 : set ⇒ order_rel (setprod R R) (1,0) z0) p HpSq) to the current goal.
We prove the intermediate claim Hap: order_rel (setprod R R) (1,0) p.
rewrite the current goal using HpEq1 (from left to right) at position 1.
rewrite the current goal using Hx1 (from left to right) at position 1.
An exact proof term for the current goal is (order_rel_setprod_R_R_same_first 1 0 1 Rlt_0_1).
An exact proof term for the current goal is Hap.
We prove the intermediate claim HcapEq: U1 ∩ ordsq_A = Empty.
We prove the intermediate claim Hsub: U1 ∩ ordsq_A ⊆ Empty.
Let z be given.
Assume Hz: z ∈ U1 ∩ ordsq_A.
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_A z Hz).
We prove the intermediate claim HzA: z ∈ ordsq_A.
An exact proof term for the current goal is (binintersectE2 U1 ordsq_A z Hz).
We prove the intermediate claim Hrel: order_rel (setprod R R) (1,0) z.
An exact proof term for the current goal is (SepE2 ordered_square (λz0 : set ⇒ order_rel (setprod R R) (1,0) z0) z HzU1).
Apply (ReplE_impred (ω ∖ {0}) (λn : set ⇒ (inv_nat n,0)) z HzA False) to the current goal.
Let n be given.
Assume HnIn: n ∈ ω ∖ {0}.
Assume HzEq: z = (inv_nat n,0).
We prove the intermediate claim Hrel': order_rel (setprod R R) (1,0) (inv_nat n,0).
rewrite the current goal using HzEq (from right to left) at position 1.
An exact proof term for the current goal is Hrel.
We prove the intermediate claim Hdisj: Rlt 1 (inv_nat n) ∨ (1 = inv_nat n ∧ Rlt 0 0).
An exact proof term for the current goal is (order_rel_setprod_R_R_disj 1 0 (inv_nat n) 0 Hrel').
Apply Hdisj to the current goal.
Assume H1ltinv: Rlt 1 (inv_nat n).
Apply FalseE to the current goal.
We prove the intermediate claim Hinvle1: Rle (inv_nat n) 1.
An exact proof term for the current goal is (inv_nat_Rle_1_local n HnIn).
We prove the intermediate claim Hnot: ¬ (Rlt 1 (inv_nat n)).
An exact proof term for the current goal is (RleE_nlt (inv_nat n) 1 Hinvle1).
An exact proof term for the current goal is (Hnot H1ltinv).
Assume HeqAnd.
Apply FalseE to the current goal.
We prove the intermediate claim Hlt: Rlt 0 0.
An exact proof term for the current goal is (andER (1 = inv_nat n) (Rlt 0 0) HeqAnd).
An exact proof term for the current goal is (not_Rlt_refl 0 real_0 Hlt).
An exact proof term for the current goal is (Empty_Subq_eq (U1 ∩ ordsq_A) Hsub).
An exact proof term for the current goal is ((Hcond U1 HU1top HpU1) HcapEq).
Assume Hxneq1: ¬ (x = 1).
Set F to be the term K_set ∩ {t ∈ R|Rlt x t}.
We prove the intermediate claim HFfin: finite F.
An exact proof term for the current goal is (K_set_above_positive_bound_finite x HxR Hxpos).
We prove the intermediate claim HallS: ∀t ∈ F, SNo t.
Let t be given.
Assume HtF.
We prove the intermediate claim HtK: t ∈ K_set.
An exact proof term for the current goal is (binintersectE1 K_set {t0 ∈ R|Rlt x t0} t HtF).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (K_set_Subq_R t HtK).
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim HxPropUI: ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x).
An exact proof term for the current goal is (SepE2 R (λt0 : set ⇒ ¬ (Rlt t0 0) ∧ ¬ (Rlt 1 t0)) x HxI).
We prove the intermediate claim Hnot1x: ¬ (Rlt 1 x).
An exact proof term for the current goal is (andER (¬ (Rlt x 0)) (¬ (Rlt 1 x)) HxPropUI).
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.
We prove the intermediate claim H1ltxR: Rlt 1 x.
An exact proof term for the current goal is (RltI 1 x real_1 HxR H1ltx).
An exact proof term for the current goal is (Hnot1x H1ltxR).
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 (Hxneq1 Hxeq1).
Assume Hxlt1': x < 1.
An exact proof term for the current goal is (RltI x 1 HxR real_1 Hxlt1').
We prove the intermediate claim H1Above: 1 ∈ {t ∈ R|Rlt x t}.
Apply (SepI R (λt0 : set ⇒ Rlt x t0) 1 real_1) to the current goal.
An exact proof term for the current goal is Hxlt1.
We prove the intermediate claim H1F: 1 ∈ F.
An exact proof term for the current goal is (binintersectI K_set {t ∈ R|Rlt x t} 1 one_in_K_set H1Above).
We prove the intermediate claim HFne0: F ≠ 0.
Assume HF0: F = 0.
We prove the intermediate claim H1in0: 1 ∈ 0.
rewrite the current goal using HF0 (from right to left) at position 2.
An exact proof term for the current goal is H1F.
An exact proof term for the current goal is (EmptyE 1 H1in0).
We prove the intermediate claim Hexm: ∃m : set, SNo_min_of F m.
An exact proof term for the current goal is (finite_min_exists F HallS HFfin HFne0).
Apply Hexm to the current goal.
Let m be given.
Assume HmMin.
We prove the intermediate claim HmPair: m ∈ F ∧ SNo m.
An exact proof term for the current goal is (andEL (m ∈ F ∧ SNo m) (∀y ∈ F, SNo y → m ≤ y) HmMin).
We prove the intermediate claim HmInF: m ∈ F.
An exact proof term for the current goal is (andEL (m ∈ F) (SNo m) HmPair).
We prove the intermediate claim HmS: SNo m.
An exact proof term for the current goal is (andER (m ∈ F) (SNo m) HmPair).
We prove the intermediate claim HmProp: ∀y ∈ F, SNo y → m ≤ y.
An exact proof term for the current goal is (andER (m ∈ F ∧ SNo m) (∀y ∈ F, SNo y → m ≤ y) HmMin).
We prove the intermediate claim HmAbove: m ∈ {t ∈ R|Rlt x t}.
An exact proof term for the current goal is (binintersectE2 K_set {t ∈ R|Rlt x t} m HmInF).
We prove the intermediate claim HmR: m ∈ R.
An exact proof term for the current goal is (SepE1 R (λt0 : set ⇒ Rlt x t0) m HmAbove).
We prove the intermediate claim Hxltm: Rlt x m.
An exact proof term for the current goal is (SepE2 R (λt0 : set ⇒ Rlt x t0) m HmAbove).
We prove the intermediate claim HmK: m ∈ K_set.
An exact proof term for the current goal is (binintersectE1 K_set {t ∈ R|Rlt x t} m HmInF).
We prove the intermediate claim HexnM: ∃n ∈ ω ∖ {0}, m = inv_nat n.
An exact proof term for the current goal is (ReplE (ω ∖ {0}) (λn0 : set ⇒ inv_nat n0) m HmK).
We prove the intermediate claim HmU: m ∈ unit_interval.
Apply HexnM to the current goal.
Let n be given.
Assume Hnpack.
Apply Hnpack to the current goal.
Assume HnIn Hmeq.
rewrite the current goal using Hmeq (from left to right).
An exact proof term for the current goal is (inv_nat_in_unit_interval n HnIn).
We prove the intermediate claim HmUprop: ¬ (Rlt m 0) ∧ ¬ (Rlt 1 m).
An exact proof term for the current goal is (SepE2 R (λt0 : set ⇒ ¬ (Rlt t0 0) ∧ ¬ (Rlt 1 t0)) m HmU).
We prove the intermediate claim Hnot1m: ¬ (Rlt 1 m).
An exact proof term for the current goal is (andER (¬ (Rlt m 0)) (¬ (Rlt 1 m)) HmUprop).
We prove the intermediate claim Hexq: ∃q : set, q ∈ rational_numbers ∧ (Rlt x q ∧ Rlt q m).
An exact proof term for the current goal is (rational_dense_between_reals x m HxR HmR Hxltm).
Apply Hexq to the current goal.
Let q be given.
Assume Hqpack.
We prove the intermediate claim HqQ: q ∈ rational_numbers.
An exact proof term for the current goal is (andEL (q ∈ rational_numbers) (Rlt x q ∧ Rlt q m) Hqpack).
We prove the intermediate claim Hqprop: Rlt x q ∧ Rlt q m.
An exact proof term for the current goal is (andER (q ∈ rational_numbers) (Rlt x q ∧ Rlt q m) Hqpack).
We prove the intermediate claim Hxltq: Rlt x q.
An exact proof term for the current goal is (andEL (Rlt x q) (Rlt q m) Hqprop).
We prove the intermediate claim Hqltm: Rlt q m.
An exact proof term for the current goal is (andER (Rlt x q) (Rlt q m) Hqprop).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (Rlt_tra 0 x q Hxpos Hxltq).
We prove the intermediate claim Hnltq0: ¬ (Rlt q 0).
An exact proof term for the current goal is (not_Rlt_sym 0 q H0ltq).
We prove the intermediate claim Hnlt1q: ¬ (Rlt 1 q).
Assume H1ltq: Rlt 1 q.
We prove the intermediate claim H1ltm: Rlt 1 m.
An exact proof term for the current goal is (Rlt_tra 1 q m H1ltq Hqltm).
An exact proof term for the current goal is (Hnot1m H1ltm).
We prove the intermediate claim HqU: q ∈ unit_interval.
Apply (SepI R (λt0 : set ⇒ ¬ (Rlt t0 0) ∧ ¬ (Rlt 1 t0)) q HqR) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hnltq0.
An exact proof term for the current goal is Hnlt1q.
Set x2 to be the term q.
We prove the intermediate claim Hx2R: x2 ∈ R.
An exact proof term for the current goal is HqR.
We prove the intermediate claim Hx2U: x2 ∈ unit_interval.
An exact proof term for the current goal is HqU.
We prove the intermediate claim Hxltx2: Rlt x x2.
An exact proof term for the current goal is Hxltq.
We prove the intermediate claim Hx2ltm: Rlt x2 m.
An exact proof term for the current goal is Hqltm.
Set U to be the term {z ∈ ordered_square|order_rel (setprod R R) (x,eps_ 1) z ∧ order_rel (setprod R R) z (x2,0)}.
We prove the intermediate claim HUpow: U ∈ 𝒫 ordered_square.
An exact proof term for the current goal is (Sep_In_Power ordered_square (λz0 : set ⇒ order_rel (setprod R R) (x,eps_ 1) z0 ∧ order_rel (setprod R R) z0 (x2,0))).
We prove the intermediate claim Ha0Sq: (x,eps_ 1) ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval x (eps_ 1) HxI eps_1_in_unit_interval).
We prove the intermediate claim Hb0Sq: (x2,0) ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval x2 0 Hx2U zero_in_unit_interval).
We prove the intermediate claim HUbas: U ∈ ordered_square_order_basis.
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 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) (λI : set ⇒ ∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, I = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}) U HUpow) to the current goal.
We use (x,eps_ 1) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0Sq.
We use (x2,0) 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 HUtop: U ∈ 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 U HUpow HUbas).
We prove the intermediate claim HpU: p ∈ U.
Apply (SepI ordered_square (λz0 : set ⇒ order_rel (setprod R R) (x,eps_ 1) z0 ∧ order_rel (setprod R R) z0 (x2,0)) p HpSq) to the current goal.
We prove the intermediate claim Hleft: order_rel (setprod R R) (x,eps_ 1) p.
rewrite the current goal using HpEq1 (from left to right) at position 2.
Apply (order_rel_setprod_R_R_intro x (eps_ 1) x 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_lt1_R.
We prove the intermediate claim Hright: order_rel (setprod R R) p (x2,0).
rewrite the current goal using HpEq1 (from left to right) at position 1.
Apply (order_rel_setprod_R_R_intro x 1 x2 0) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Hxltx2.
An exact proof term for the current goal is (andI (order_rel (setprod R R) (x,eps_ 1) p) (order_rel (setprod R R) p (x2,0)) Hleft Hright).
We prove the intermediate claim HcapEq: U ∩ ordsq_A = Empty.
We prove the intermediate claim Hsub: U ∩ ordsq_A ⊆ Empty.
Let w be given.
Assume Hw: w ∈ U ∩ ordsq_A.
We will prove w ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HwU: w ∈ U.
An exact proof term for the current goal is (binintersectE1 U ordsq_A w Hw).
We prove the intermediate claim HwA: w ∈ ordsq_A.
An exact proof term for the current goal is (binintersectE2 U ordsq_A w Hw).
We prove the intermediate claim HexnA: ∃n ∈ ω ∖ {0}, w = (inv_nat n,0).
An exact proof term for the current goal is (ReplE (ω ∖ {0}) (λm0 : set ⇒ (inv_nat m0,0)) w HwA).
Apply HexnA to the current goal.
Let n be given.
Assume Hnpack.
Apply Hnpack to the current goal.
Assume HnIn Hweq.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (setminusE1 ω {0} n HnIn).
We prove the intermediate claim HinvR: inv_nat n ∈ R.
An exact proof term for the current goal is (inv_nat_real n HnO).
We prove the intermediate claim HinvS: SNo (inv_nat n).
An exact proof term for the current goal is (real_SNo (inv_nat n) HinvR).
We prove the intermediate claim HinvK: inv_nat n ∈ K_set.
An exact proof term for the current goal is (ReplI (ω ∖ {0}) (λn0 : set ⇒ inv_nat n0) n HnIn).
We prove the intermediate claim HordPack: order_rel (setprod R R) (x,eps_ 1) w ∧ order_rel (setprod R R) w (x2,0).
An exact proof term for the current goal is (SepE2 ordered_square (λz0 : set ⇒ order_rel (setprod R R) (x,eps_ 1) z0 ∧ order_rel (setprod R R) z0 (x2,0)) w HwU).
We prove the intermediate claim Hord1: order_rel (setprod R R) (x,eps_ 1) w.
An exact proof term for the current goal is (andEL (order_rel (setprod R R) (x,eps_ 1) w) (order_rel (setprod R R) w (x2,0)) HordPack).
We prove the intermediate claim Hord2: order_rel (setprod R R) w (x2,0).
An exact proof term for the current goal is (andER (order_rel (setprod R R) (x,eps_ 1) w) (order_rel (setprod R R) w (x2,0)) HordPack).
We prove the intermediate claim Hord1': order_rel (setprod R R) (x,eps_ 1) (inv_nat n,0).
rewrite the current goal using Hweq (from right to left) at position 1.
An exact proof term for the current goal is Hord1.
We prove the intermediate claim Hord2': order_rel (setprod R R) (inv_nat n,0) (x2,0).
rewrite the current goal using Hweq (from right to left) at position 1.
An exact proof term for the current goal is Hord2.
We prove the intermediate claim Hdisj1: Rlt x (inv_nat n) ∨ (x = inv_nat n ∧ Rlt (eps_ 1) 0).
An exact proof term for the current goal is (order_rel_setprod_R_R_disj x (eps_ 1) (inv_nat n) 0 Hord1').
We prove the intermediate claim HxltInv: Rlt x (inv_nat n).
Apply Hdisj1 to the current goal.
Assume Hlt.
An exact proof term for the current goal is Hlt.
Assume Hbad.
Apply FalseE to the current goal.
We prove the intermediate claim Heps0: Rlt (eps_ 1) 0.
An exact proof term for the current goal is (andER (x = inv_nat n) (Rlt (eps_ 1) 0) Hbad).
An exact proof term for the current goal is ((not_Rlt_sym 0 (eps_ 1) eps_1_pos_R) Heps0).
We prove the intermediate claim Hdisj2: Rlt (inv_nat n) x2 ∨ (inv_nat n = x2 ∧ Rlt 0 0).
An exact proof term for the current goal is (order_rel_setprod_R_R_disj (inv_nat n) 0 x2 0 Hord2').
We prove the intermediate claim HinvLtx2: Rlt (inv_nat n) x2.
Apply Hdisj2 to the current goal.
Assume Hlt.
An exact proof term for the current goal is Hlt.
Assume Hbad.
Apply FalseE to the current goal.
We prove the intermediate claim H00: Rlt 0 0.
An exact proof term for the current goal is (andER (inv_nat n = x2) (Rlt 0 0) Hbad).
An exact proof term for the current goal is (not_Rlt_refl 0 real_0 H00).
We prove the intermediate claim HinvInAbove: (inv_nat n) ∈ {t ∈ R|Rlt x t}.
Apply (SepI R (λt0 : set ⇒ Rlt x t0) (inv_nat n) HinvR) to the current goal.
An exact proof term for the current goal is HxltInv.
We prove the intermediate claim HinvInF: (inv_nat n) ∈ F.
An exact proof term for the current goal is (binintersectI K_set {t ∈ R|Rlt x t} (inv_nat n) HinvK HinvInAbove).
We prove the intermediate claim HmLeInv: m ≤ (inv_nat n).
An exact proof term for the current goal is (HmProp (inv_nat n) HinvInF HinvS).
We prove the intermediate claim HinvLtS: inv_nat n < x2.
An exact proof term for the current goal is (RltE_lt (inv_nat n) x2 HinvLtx2).
We prove the intermediate claim Hx2LtS: x2 < m.
An exact proof term for the current goal is (RltE_lt x2 m Hx2ltm).
We prove the intermediate claim HinvLtM: inv_nat n < m.
An exact proof term for the current goal is (SNoLt_tra (inv_nat n) x2 m HinvS (real_SNo x2 Hx2R) HmS HinvLtS Hx2LtS).
We prove the intermediate claim Hmm: m < m.
An exact proof term for the current goal is (SNoLeLt_tra m (inv_nat n) m HmS HinvS HmS HmLeInv HinvLtM).
An exact proof term for the current goal is ((SNoLt_irref m) Hmm).
An exact proof term for the current goal is (Empty_Subq_eq (U ∩ ordsq_A) Hsub).
An exact proof term for the current goal is ((Hcond U HUtop HpU) HcapEq).
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 (Hnot1y H1ltyR).
Assume Heq: p01 = p.
Apply binunionI2 to the current goal.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is (SingI p01).
Assume Hpp01: order_rel (setprod R R) p p01.
Apply FalseE to the current goal.
Set U to be the term {z ∈ ordered_square|order_rel (setprod R R) z p01}.
We prove the intermediate claim HUpow: U ∈ 𝒫 ordered_square.
Apply (PowerI ordered_square U) to the current goal.
Let z be given.
Assume Hz: z ∈ U.
An exact proof term for the current goal is (SepE1 ordered_square (λz0 : set ⇒ order_rel (setprod R R) z0 p01) z Hz).
We prove the intermediate claim HUbas: U ∈ ordered_square_order_basis.
Set Bint to be the term {J ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, ∃b0 ∈ ordered_square, J = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0 ∧ order_rel (setprod R R) x0 b0}}.
Set Blow to be the term {J ∈ 𝒫 ordered_square|∃b0 ∈ ordered_square, J = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}}.
Set Bup to be the term {J ∈ 𝒫 ordered_square|∃a0 ∈ ordered_square, J = {x0 ∈ ordered_square|order_rel (setprod R R) a0 x0}}.
We prove the intermediate claim HUinBlow: U ∈ Blow.
Apply (SepI (𝒫 ordered_square) (λJ0 : set ⇒ ∃b0 ∈ ordered_square, J0 = {x0 ∈ ordered_square|order_rel (setprod R R) x0 b0}) U HUpow) to the current goal.
We use p01 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hp01Sq.
Use reflexivity.
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.
An exact proof term for the current goal is HUinBlow.
We prove the intermediate claim HUtop: U ∈ 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 U HUpow HUbas).
We prove the intermediate claim HpU: p ∈ U.
Apply (SepI ordered_square (λz0 : set ⇒ order_rel (setprod R R) z0 p01) p HpSq) to the current goal.
An exact proof term for the current goal is Hpp01.
We prove the intermediate claim HcapSub: U ∩ ordsq_A ⊆ Empty.
Let w be given.
Assume Hw: w ∈ U ∩ ordsq_A.
We will prove w ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HwA: w ∈ ordsq_A.
An exact proof term for the current goal is (binintersectE2 U ordsq_A w Hw).
We prove the intermediate claim HwU: w ∈ U.
An exact proof term for the current goal is (binintersectE1 U ordsq_A w Hw).
We prove the intermediate claim Hexm: ∃m ∈ ω ∖ {0}, w = (inv_nat m,0).
An exact proof term for the current goal is (ReplE (ω ∖ {0}) (λm0 : set ⇒ (inv_nat m0,0)) w HwA).
Apply Hexm to the current goal.
Let m be given.
Assume Hmpack.
Apply Hmpack to the current goal.
Assume HmIn Hweq.
We prove the intermediate claim Hinvpos: Rlt 0 (inv_nat m).
An exact proof term for the current goal is (inv_nat_pos m HmIn).
We prove the intermediate claim Hrelwp01: order_rel (setprod R R) (inv_nat m,0) (0,1).
We prove the intermediate claim Hrel: order_rel (setprod R R) (inv_nat m,0) p01.
rewrite the current goal using Hweq (from right to left).
An exact proof term for the current goal is (SepE2 ordered_square (λz0 : set ⇒ order_rel (setprod R R) z0 p01) w HwU).
rewrite the current goal using Hp01def (from right to left).
An exact proof term for the current goal is Hrel.
We prove the intermediate claim Hex: ∃c1 c2 d1 d2 : set, (inv_nat m,0) = (c1,c2) ∧ (0,1) = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).
An exact proof term for the current goal is (order_rel_setprod_R_R_unfold (inv_nat m,0) (0,1) Hrelwp01).
Apply Hex to the current goal.
Let c1 be given.
Assume Hc1.
Apply Hc1 to the current goal.
Let c2 be given.
Assume Hd1.
Apply Hd1 to the current goal.
Let d1 be given.
Assume Hd2.
Apply Hd2 to the current goal.
Let d2 be given.
Assume Hcore.
Apply Hcore to the current goal.
Assume Hpair Hdisj.
Apply Hdisj to the current goal.
Assume Hlt: Rlt c1 d1.
We prove the intermediate claim Heq1: (inv_nat m,0) = (c1,c2).
An exact proof term for the current goal is (andEL ((inv_nat m,0) = (c1,c2)) ((0,1) = (d1,d2)) Hpair).
We prove the intermediate claim Heq2: (0,1) = (d1,d2).
An exact proof term for the current goal is (andER ((inv_nat m,0) = (c1,c2)) ((0,1) = (d1,d2)) Hpair).
We prove the intermediate claim Hc1eq: c1 = inv_nat m.
We prove the intermediate claim H0eq: (inv_nat m,0) 0 = (c1,c2) 0.
rewrite the current goal using Heq1 (from left to right).
Use reflexivity.
We prove the intermediate claim Htmp: inv_nat m = c1.
rewrite the current goal using (tuple_2_0_eq (inv_nat m) 0) (from right to left).
rewrite the current goal using (tuple_2_0_eq c1 c2) (from right to left).
An exact proof term for the current goal is H0eq.
rewrite the current goal using Htmp (from right to left).
Use reflexivity.
We prove the intermediate claim Hd1eq: d1 = 0.
We prove the intermediate claim H0eq: (0,1) 0 = (d1,d2) 0.
rewrite the current goal using Heq2 (from left to right).
Use reflexivity.
We prove the intermediate claim Htmp: 0 = d1.
rewrite the current goal using (tuple_2_0_eq 0 1) (from right to left).
rewrite the current goal using (tuple_2_0_eq d1 d2) (from right to left).
An exact proof term for the current goal is H0eq.
rewrite the current goal using Htmp (from right to left).
Use reflexivity.
We prove the intermediate claim Hbad: Rlt (inv_nat m) 0.
rewrite the current goal using Hc1eq (from right to left).
rewrite the current goal using Hd1eq (from right to left).
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is ((not_Rlt_sym 0 (inv_nat m) Hinvpos) Hbad).
Assume Heq2: c1 = d1 ∧ Rlt c2 d2.
We prove the intermediate claim Heq1': (inv_nat m,0) = (c1,c2).
An exact proof term for the current goal is (andEL ((inv_nat m,0) = (c1,c2)) ((0,1) = (d1,d2)) Hpair).
We prove the intermediate claim Heq2': (0,1) = (d1,d2).
An exact proof term for the current goal is (andER ((inv_nat m,0) = (c1,c2)) ((0,1) = (d1,d2)) Hpair).
We prove the intermediate claim Hc1eq: c1 = inv_nat m.
We prove the intermediate claim H0eq: (inv_nat m,0) 0 = (c1,c2) 0.
rewrite the current goal using Heq1' (from left to right).
Use reflexivity.
We prove the intermediate claim Htmp: inv_nat m = c1.
rewrite the current goal using (tuple_2_0_eq (inv_nat m) 0) (from right to left).
rewrite the current goal using (tuple_2_0_eq c1 c2) (from right to left).
An exact proof term for the current goal is H0eq.
rewrite the current goal using Htmp (from right to left).
Use reflexivity.
We prove the intermediate claim Hd1eq: d1 = 0.
We prove the intermediate claim H0eq: (0,1) 0 = (d1,d2) 0.
rewrite the current goal using Heq2' (from left to right).
Use reflexivity.
We prove the intermediate claim Htmp: 0 = d1.
rewrite the current goal using (tuple_2_0_eq 0 1) (from right to left).
rewrite the current goal using (tuple_2_0_eq d1 d2) (from right to left).
An exact proof term for the current goal is H0eq.
rewrite the current goal using Htmp (from right to left).
Use reflexivity.
We prove the intermediate claim Hc1eqd1: inv_nat m = 0.
We prove the intermediate claim Hc1d1: c1 = d1.
An exact proof term for the current goal is (andEL (c1 = d1) (Rlt c2 d2) Heq2).
rewrite the current goal using Hc1eq (from right to left).
rewrite the current goal using Hc1d1 (from left to right).
An exact proof term for the current goal is Hd1eq.
We prove the intermediate claim Hbad: Rlt 0 0.
rewrite the current goal using Hc1eqd1 (from right to left) at position 2.
An exact proof term for the current goal is Hinvpos.
An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) Hbad).
We prove the intermediate claim HcapEq: U ∩ ordsq_A = Empty.
An exact proof term for the current goal is (Empty_Subq_eq (U ∩ ordsq_A) HcapSub).
An exact proof term for the current goal is ((Hcond U HUtop HpU) HcapEq).
∎