We will prove closed_in (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology Sorgenfrey_plane_L.
Set X to be the term setprod Sorgenfrey_line Sorgenfrey_line.
Set Tx to be the term Sorgenfrey_plane_topology.
Set L to be the term Sorgenfrey_plane_L.
Set B to be the term product_subbasis Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line Sorgenfrey_topology.
We prove the intermediate claim HTline: topology_on Sorgenfrey_line Sorgenfrey_topology.
An exact proof term for the current goal is R_lower_limit_topology_is_topology.
We prove the intermediate claim HBasis: basis_on X B.
An exact proof term for the current goal is (product_subbasis_is_basis Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line Sorgenfrey_topology HTline HTline).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (lemma_topology_from_basis X B HBasis).
We prove the intermediate claim HLsub: L ⊆ X.
Let p be given.
Assume HpL: p ∈ L.
We prove the intermediate claim Hex: ∃x ∈ R, p = (x,minus_SNo x).
An exact proof term for the current goal is (ReplE R (λx0 : set ⇒ (x0,minus_SNo x0)) p HpL).
Apply Hex to the current goal.
Let x be given.
Assume Hxpair: x ∈ R ∧ p = (x,minus_SNo x).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (andEL (x ∈ R) (p = (x,minus_SNo x)) Hxpair).
We prove the intermediate claim Hpeq: p = (x,minus_SNo x).
An exact proof term for the current goal is (andER (x ∈ R) (p = (x,minus_SNo x)) Hxpair).
We prove the intermediate claim HmxR: (minus_SNo x) ∈ R.
An exact proof term for the current goal is (real_minus_SNo x HxR).
rewrite the current goal using Hpeq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x (minus_SNo x) HxR HmxR).
Set U to be the term X ∖ L.
We prove the intermediate claim HUinT: U ∈ Tx.
We prove the intermediate claim HTdef: Tx = generated_topology X B.
Use reflexivity.
rewrite the current goal using HTdef (from left to right).
We will prove U ∈ generated_topology X B.
We prove the intermediate claim HUpow: U ∈ 𝒫 X.
An exact proof term for the current goal is (setminus_In_Power X L).
We prove the intermediate claim HUloc: ∀p ∈ U, ∃b ∈ B, p ∈ b ∧ b ⊆ U.
Let p be given.
Assume HpU: p ∈ U.
We prove the intermediate claim HpX: p ∈ X.
An exact proof term for the current goal is (setminusE1 X L p HpU).
We prove the intermediate claim HpnotL: p ∉ L.
An exact proof term for the current goal is (setminusE2 X L p HpU).
We prove the intermediate claim Hp0R: (p 0) ∈ R.
An exact proof term for the current goal is (ap0_Sigma R (λ_ : set ⇒ R) p HpX).
We prove the intermediate claim Hp1R: (p 1) ∈ R.
An exact proof term for the current goal is (ap1_Sigma R (λ_ : set ⇒ R) p HpX).
We prove the intermediate claim Hm0R: (minus_SNo (p 0)) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (p 0) Hp0R).
We prove the intermediate claim Hp0S: SNo (p 0).
An exact proof term for the current goal is (real_SNo (p 0) Hp0R).
We prove the intermediate claim Hp1S: SNo (p 1).
An exact proof term for the current goal is (real_SNo (p 1) Hp1R).
We prove the intermediate claim Hm0S: SNo (minus_SNo (p 0)).
An exact proof term for the current goal is (real_SNo (minus_SNo (p 0)) Hm0R).
Apply (SNoLt_trichotomy_or_impred (p 1) (minus_SNo (p 0)) Hp1S Hm0S (∃b ∈ B, p ∈ b ∧ b ⊆ U)) to the current goal.
Assume Hylt: (p 1) < (minus_SNo (p 0)).
We prove the intermediate claim HyltR: Rlt (p 1) (minus_SNo (p 0)).
An exact proof term for the current goal is (RltI (p 1) (minus_SNo (p 0)) Hp1R Hm0R Hylt).
We prove the intermediate claim Hexq: ∃q ∈ rational_numbers, Rlt (p 1) q ∧ Rlt q (minus_SNo (p 0)).
An exact proof term for the current goal is (rational_dense_between_reals (p 1) (minus_SNo (p 0)) Hp1R Hm0R HyltR).
Apply Hexq to the current goal.
Let q be given.
Assume Hqpair.
We prove the intermediate claim HqQ: q ∈ rational_numbers.
An exact proof term for the current goal is (andEL (q ∈ rational_numbers) (Rlt (p 1) q ∧ Rlt q (minus_SNo (p 0))) Hqpair).
We prove the intermediate claim Hqprop: Rlt (p 1) q ∧ Rlt q (minus_SNo (p 0)).
An exact proof term for the current goal is (andER (q ∈ rational_numbers) (Rlt (p 1) q ∧ Rlt q (minus_SNo (p 0))) Hqpair).
We prove the intermediate claim Hp1q: Rlt (p 1) q.
An exact proof term for the current goal is (andEL (Rlt (p 1) q) (Rlt q (minus_SNo (p 0))) Hqprop).
We prove the intermediate claim Hq_m0: Rlt q (minus_SNo (p 0)).
An exact proof term for the current goal is (andER (Rlt (p 1) q) (Rlt q (minus_SNo (p 0))) 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 HqS: SNo q.
An exact proof term for the current goal is (real_SNo q HqR).
We prove the intermediate claim HmqR: (minus_SNo q) ∈ R.
An exact proof term for the current goal is (real_minus_SNo q HqR).
We prove the intermediate claim Hq_m0_lt: q < (minus_SNo (p 0)).
An exact proof term for the current goal is (RltE_lt q (minus_SNo (p 0)) Hq_m0).
We prove the intermediate claim Hp0_lt_mq: (p 0) < (minus_SNo q).
An exact proof term for the current goal is (minus_SNo_Lt_contra2 q (p 0) HqS Hp0S Hq_m0_lt).
We prove the intermediate claim Hp0mq: Rlt (p 0) (minus_SNo q).
An exact proof term for the current goal is (RltI (p 0) (minus_SNo q) Hp0R HmqR Hp0_lt_mq).
Set U0 to be the term halfopen_interval_left (p 0) (minus_SNo q).
Set V0 to be the term halfopen_interval_left (p 1) q.
We prove the intermediate claim HU0T: U0 ∈ Sorgenfrey_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology (p 0) (minus_SNo q) Hp0R HmqR).
We prove the intermediate claim HV0T: V0 ∈ Sorgenfrey_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology (p 1) q Hp1R HqR).
We prove the intermediate claim HbB: rectangle_set U0 V0 ∈ B.
We will prove rectangle_set U0 V0 ∈ product_subbasis R R_lower_limit_topology R R_lower_limit_topology.
We prove the intermediate claim HbRepl: rectangle_set U0 V0 ∈ {rectangle_set U0 V|V ∈ R_lower_limit_topology}.
An exact proof term for the current goal is (ReplI R_lower_limit_topology (λV : set ⇒ rectangle_set U0 V) V0 HV0T).
An exact proof term for the current goal is (famunionI R_lower_limit_topology (λUx : set ⇒ {rectangle_set Ux V|V ∈ R_lower_limit_topology}) U0 (rectangle_set U0 V0) HU0T HbRepl).
We prove the intermediate claim HpU0: (p 0) ∈ U0.
An exact proof term for the current goal is (halfopen_interval_left_leftmem (p 0) (minus_SNo q) Hp0mq).
We prove the intermediate claim HpV0: (p 1) ∈ V0.
An exact proof term for the current goal is (halfopen_interval_left_leftmem (p 1) q Hp1q).
We prove the intermediate claim Hpb: p ∈ rectangle_set U0 V0.
We prove the intermediate claim HpEta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta R R p HpX).
rewrite the current goal using HpEta (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_rectangle_set U0 V0 (p 0) (p 1) HpU0 HpV0).
We prove the intermediate claim HbSub: rectangle_set U0 V0 ⊆ U.
Let z be given.
Assume Hz: z ∈ rectangle_set U0 V0.
We will prove z ∈ U.
We prove the intermediate claim HzX: z ∈ X.
We prove the intermediate claim HzProd: z ∈ setprod U0 V0.
rewrite the current goal using rectangle_set_def (from right to left).
An exact proof term for the current goal is Hz.
An exact proof term for the current goal is (setprod_Subq U0 V0 R R (halfopen_interval_left_Subq_R (p 0) (minus_SNo q)) (halfopen_interval_left_Subq_R (p 1) q) z HzProd).
Apply setminusI X L z HzX to the current goal.
Assume HzL: z ∈ L.
We prove the intermediate claim Hext: ∃t ∈ R, z = (t,minus_SNo t).
An exact proof term for the current goal is (ReplE R (λt0 : set ⇒ (t0,minus_SNo t0)) z HzL).
Apply Hext to the current goal.
Let t be given.
Assume Htpair.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (andEL (t ∈ R) (z = (t,minus_SNo t)) Htpair).
We prove the intermediate claim Hzeq: z = (t,minus_SNo t).
An exact proof term for the current goal is (andER (t ∈ R) (z = (t,minus_SNo t)) Htpair).
We prove the intermediate claim HmtR: (minus_SNo t) ∈ R.
An exact proof term for the current goal is (real_minus_SNo t HtR).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HmtS: SNo (minus_SNo t).
An exact proof term for the current goal is (real_SNo (minus_SNo t) HmtR).
We prove the intermediate claim Hz0: z 0 = t.
rewrite the current goal using Hzeq (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq t (minus_SNo t)).
We prove the intermediate claim Hz1: z 1 = minus_SNo t.
rewrite the current goal using Hzeq (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq t (minus_SNo t)).
We prove the intermediate claim Hz0U0: (z 0) ∈ U0.
We prove the intermediate claim HzProd: z ∈ setprod U0 V0.
rewrite the current goal using rectangle_set_def (from right to left).
An exact proof term for the current goal is Hz.
An exact proof term for the current goal is (ap0_Sigma U0 (λ_ : set ⇒ V0) z HzProd).
We prove the intermediate claim Hz1V0: (z 1) ∈ V0.
We prove the intermediate claim HzProd: z ∈ setprod U0 V0.
rewrite the current goal using rectangle_set_def (from right to left).
An exact proof term for the current goal is Hz.
An exact proof term for the current goal is (ap1_Sigma U0 (λ_ : set ⇒ V0) z HzProd).
We prove the intermediate claim HtU0: t ∈ U0.
rewrite the current goal using Hz0 (from right to left).
An exact proof term for the current goal is Hz0U0.
We prove the intermediate claim HmtV0: (minus_SNo t) ∈ V0.
rewrite the current goal using Hz1 (from right to left).
An exact proof term for the current goal is Hz1V0.
We prove the intermediate claim HtU0prop: ¬ (Rlt t (p 0)) ∧ Rlt t (minus_SNo q).
An exact proof term for the current goal is (SepE2 R (λu : set ⇒ ¬ (Rlt u (p 0)) ∧ Rlt u (minus_SNo q)) t HtU0).
We prove the intermediate claim Ht_lt_mq: Rlt t (minus_SNo q).
An exact proof term for the current goal is (andER (¬ (Rlt t (p 0))) (Rlt t (minus_SNo q)) HtU0prop).
We prove the intermediate claim HmtV0prop: ¬ (Rlt (minus_SNo t) (p 1)) ∧ Rlt (minus_SNo t) q.
An exact proof term for the current goal is (SepE2 R (λv : set ⇒ ¬ (Rlt v (p 1)) ∧ Rlt v q) (minus_SNo t) HmtV0).
We prove the intermediate claim Hmt_lt_q: Rlt (minus_SNo t) q.
An exact proof term for the current goal is (andER (¬ (Rlt (minus_SNo t) (p 1))) (Rlt (minus_SNo t) q) HmtV0prop).
We prove the intermediate claim Ht_lt_mq_lt: t < (minus_SNo q).
An exact proof term for the current goal is (RltE_lt t (minus_SNo q) Ht_lt_mq).
We prove the intermediate claim Hq_lt_mt: q < (minus_SNo t).
An exact proof term for the current goal is (minus_SNo_Lt_contra2 t q HtS HqS Ht_lt_mq_lt).
We prove the intermediate claim Hq_lt_mtR: Rlt q (minus_SNo t).
An exact proof term for the current goal is (RltI q (minus_SNo t) HqR HmtR Hq_lt_mt).
An exact proof term for the current goal is ((not_Rlt_sym q (minus_SNo t) Hq_lt_mtR) Hmt_lt_q).
We use (rectangle_set U0 V0) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbB.
Apply andI to the current goal.
An exact proof term for the current goal is Hpb.
An exact proof term for the current goal is HbSub.
Assume Hyeq: (p 1) = (minus_SNo (p 0)).
Apply FalseE to the current goal.
We prove the intermediate claim HpEta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta R R p HpX).
We prove the intermediate claim Htuple: (p 0,p 1) = (p 0,minus_SNo (p 0)).
Apply (tuple_2_ext (p 0) (p 1) (p 0) (minus_SNo (p 0))) to the current goal.
Use reflexivity.
An exact proof term for the current goal is Hyeq.
We prove the intermediate claim HptupleL: (p 0,p 1) ∈ L.
rewrite the current goal using Htuple (from left to right).
An exact proof term for the current goal is (ReplI R (λx0 : set ⇒ (x0,minus_SNo x0)) (p 0) Hp0R).
We prove the intermediate claim HpL: p ∈ L.
rewrite the current goal using HpEta (from left to right).
An exact proof term for the current goal is HptupleL.
An exact proof term for the current goal is (HpnotL HpL).
Assume Hlt: (minus_SNo (p 0)) < (p 1).
We prove the intermediate claim HltR: Rlt (minus_SNo (p 0)) (p 1).
An exact proof term for the current goal is (RltI (minus_SNo (p 0)) (p 1) Hm0R Hp1R Hlt).
We prove the intermediate claim Hexq: ∃q ∈ rational_numbers, Rlt (minus_SNo (p 0)) q ∧ Rlt q (p 1).
An exact proof term for the current goal is (rational_dense_between_reals (minus_SNo (p 0)) (p 1) Hm0R Hp1R HltR).
Apply Hexq to the current goal.
Let q be given.
Assume Hqpair.
We prove the intermediate claim HqQ: q ∈ rational_numbers.
An exact proof term for the current goal is (andEL (q ∈ rational_numbers) (Rlt (minus_SNo (p 0)) q ∧ Rlt q (p 1)) Hqpair).
We prove the intermediate claim Hqprop: Rlt (minus_SNo (p 0)) q ∧ Rlt q (p 1).
An exact proof term for the current goal is (andER (q ∈ rational_numbers) (Rlt (minus_SNo (p 0)) q ∧ Rlt q (p 1)) Hqpair).
We prove the intermediate claim Hm0q: Rlt (minus_SNo (p 0)) q.
An exact proof term for the current goal is (andEL (Rlt (minus_SNo (p 0)) q) (Rlt q (p 1)) Hqprop).
We prove the intermediate claim Hqy: Rlt q (p 1).
An exact proof term for the current goal is (andER (Rlt (minus_SNo (p 0)) q) (Rlt q (p 1)) 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 HqS: SNo q.
An exact proof term for the current goal is (real_SNo q HqR).
We prove the intermediate claim Hy1R: (add_SNo (p 1) 1) ∈ R.
An exact proof term for the current goal is (real_add_SNo (p 1) Hp1R 1 real_1).
We prove the intermediate claim Hy1S: SNo (add_SNo (p 1) 1).
An exact proof term for the current goal is (real_SNo (add_SNo (p 1) 1) Hy1R).
We prove the intermediate claim Hp1_lt_p11: (p 1) < (add_SNo (p 1) 1).
rewrite the current goal using (add_SNo_0R (p 1) Hp1S) (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Lt2 (p 1) 0 1 Hp1S SNo_0 SNo_1 SNoLt_0_1).
We prove the intermediate claim Hp1_lt_p11R: Rlt (p 1) (add_SNo (p 1) 1).
An exact proof term for the current goal is (RltI (p 1) (add_SNo (p 1) 1) Hp1R Hy1R Hp1_lt_p11).
We prove the intermediate claim Hq_lt_y1: Rlt q (add_SNo (p 1) 1).
An exact proof term for the current goal is (Rlt_tra q (p 1) (add_SNo (p 1) 1) Hqy Hp1_lt_p11R).
Set U0 to be the term halfopen_interval_left (p 0) (add_SNo (p 0) 1).
Set V0 to be the term halfopen_interval_left q (add_SNo (p 1) 1).
We prove the intermediate claim Hp01R: (add_SNo (p 0) 1) ∈ R.
An exact proof term for the current goal is (real_add_SNo (p 0) Hp0R 1 real_1).
We prove the intermediate claim Hp01S: SNo (add_SNo (p 0) 1).
An exact proof term for the current goal is (real_SNo (add_SNo (p 0) 1) Hp01R).
We prove the intermediate claim Hp0_lt_p01: (p 0) < (add_SNo (p 0) 1).
rewrite the current goal using (add_SNo_0R (p 0) Hp0S) (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Lt2 (p 0) 0 1 Hp0S SNo_0 SNo_1 SNoLt_0_1).
We prove the intermediate claim Hp0_lt_p01R: Rlt (p 0) (add_SNo (p 0) 1).
An exact proof term for the current goal is (RltI (p 0) (add_SNo (p 0) 1) Hp0R Hp01R Hp0_lt_p01).
We prove the intermediate claim HU0T: U0 ∈ Sorgenfrey_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology (p 0) (add_SNo (p 0) 1) Hp0R Hp01R).
We prove the intermediate claim HV0T: V0 ∈ Sorgenfrey_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology q (add_SNo (p 1) 1) HqR Hy1R).
We prove the intermediate claim HbB: (rectangle_set U0 V0) ∈ B.
We will prove (rectangle_set U0 V0) ∈ product_subbasis R R_lower_limit_topology R R_lower_limit_topology.
We prove the intermediate claim HbRepl: (rectangle_set U0 V0) ∈ {rectangle_set U0 V|V ∈ R_lower_limit_topology}.
An exact proof term for the current goal is (ReplI R_lower_limit_topology (λV : set ⇒ rectangle_set U0 V) V0 HV0T).
An exact proof term for the current goal is (famunionI R_lower_limit_topology (λUx : set ⇒ {rectangle_set Ux V|V ∈ R_lower_limit_topology}) U0 (rectangle_set U0 V0) HU0T HbRepl).
We prove the intermediate claim HpU0: (p 0) ∈ U0.
An exact proof term for the current goal is (halfopen_interval_left_leftmem (p 0) (add_SNo (p 0) 1) Hp0_lt_p01R).
We prove the intermediate claim HpV0: (p 1) ∈ V0.
We prove the intermediate claim Hnlt: ¬ (Rlt (p 1) q).
An exact proof term for the current goal is (not_Rlt_sym q (p 1) Hqy).
We prove the intermediate claim Hp1V0prop: ¬ (Rlt (p 1) q) ∧ Rlt (p 1) (add_SNo (p 1) 1).
Apply andI to the current goal.
An exact proof term for the current goal is Hnlt.
An exact proof term for the current goal is Hp1_lt_p11R.
An exact proof term for the current goal is (SepI R (λv : set ⇒ ¬ (Rlt v q) ∧ Rlt v (add_SNo (p 1) 1)) (p 1) Hp1R Hp1V0prop).
We prove the intermediate claim Hpb: p ∈ rectangle_set U0 V0.
We prove the intermediate claim HpEta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta R R p HpX).
rewrite the current goal using HpEta (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_rectangle_set U0 V0 (p 0) (p 1) HpU0 HpV0).
We prove the intermediate claim HbSub: (rectangle_set U0 V0) ⊆ U.
Let z be given.
Assume Hz: z ∈ rectangle_set U0 V0.
We will prove z ∈ U.
We prove the intermediate claim HzProd: z ∈ setprod U0 V0.
rewrite the current goal using rectangle_set_def (from right to left).
An exact proof term for the current goal is Hz.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (setprod_Subq U0 V0 R R (halfopen_interval_left_Subq_R (p 0) (add_SNo (p 0) 1)) (halfopen_interval_left_Subq_R q (add_SNo (p 1) 1)) z HzProd).
Apply setminusI X L z HzX to the current goal.
Assume HzL: z ∈ L.
We prove the intermediate claim Hext: ∃t ∈ R, z = (t,minus_SNo t).
An exact proof term for the current goal is (ReplE R (λt0 : set ⇒ (t0,minus_SNo t0)) z HzL).
Apply Hext to the current goal.
Let t be given.
Assume Htpair.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (andEL (t ∈ R) (z = (t,minus_SNo t)) Htpair).
We prove the intermediate claim Hzeq: z = (t,minus_SNo t).
An exact proof term for the current goal is (andER (t ∈ R) (z = (t,minus_SNo t)) Htpair).
We prove the intermediate claim HmtR: (minus_SNo t) ∈ R.
An exact proof term for the current goal is (real_minus_SNo t HtR).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HmtS: SNo (minus_SNo t).
An exact proof term for the current goal is (real_SNo (minus_SNo t) HmtR).
We prove the intermediate claim Hz0: z 0 = t.
rewrite the current goal using Hzeq (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq t (minus_SNo t)).
We prove the intermediate claim Hz1: z 1 = minus_SNo t.
rewrite the current goal using Hzeq (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq t (minus_SNo t)).
We prove the intermediate claim Hz0U0: (z 0) ∈ U0.
An exact proof term for the current goal is (ap0_Sigma U0 (λ_ : set ⇒ V0) z HzProd).
We prove the intermediate claim Hz1V0: (z 1) ∈ V0.
An exact proof term for the current goal is (ap1_Sigma U0 (λ_ : set ⇒ V0) z HzProd).
We prove the intermediate claim HtU0: t ∈ U0.
rewrite the current goal using Hz0 (from right to left).
An exact proof term for the current goal is Hz0U0.
We prove the intermediate claim HmtV0: (minus_SNo t) ∈ V0.
rewrite the current goal using Hz1 (from right to left).
An exact proof term for the current goal is Hz1V0.
We prove the intermediate claim HtU0prop: ¬ (Rlt t (p 0)) ∧ Rlt t (add_SNo (p 0) 1).
An exact proof term for the current goal is (SepE2 R (λu : set ⇒ ¬ (Rlt u (p 0)) ∧ Rlt u (add_SNo (p 0) 1)) t HtU0).
We prove the intermediate claim Hnlt_tx: ¬ (Rlt t (p 0)).
An exact proof term for the current goal is (andEL (¬ (Rlt t (p 0))) (Rlt t (add_SNo (p 0) 1)) HtU0prop).
We prove the intermediate claim HmtV0prop: ¬ (Rlt (minus_SNo t) q) ∧ Rlt (minus_SNo t) (add_SNo (p 1) 1).
An exact proof term for the current goal is (SepE2 R (λv : set ⇒ ¬ (Rlt v q) ∧ Rlt v (add_SNo (p 1) 1)) (minus_SNo t) HmtV0).
We prove the intermediate claim Hnlt_mt_q: ¬ (Rlt (minus_SNo t) q).
An exact proof term for the current goal is (andEL (¬ (Rlt (minus_SNo t) q)) (Rlt (minus_SNo t) (add_SNo (p 1) 1)) HmtV0prop).
Apply (SNoLt_trichotomy_or_impred (p 0) t Hp0S HtS False) to the current goal.
Assume Hp0lt: (p 0) < t.
We prove the intermediate claim Hmt_lt_m0: (minus_SNo t) < (minus_SNo (p 0)).
An exact proof term for the current goal is (minus_SNo_Lt_contra (p 0) t Hp0S HtS Hp0lt).
We prove the intermediate claim Hmt_m0: Rlt (minus_SNo t) (minus_SNo (p 0)).
An exact proof term for the current goal is (RltI (minus_SNo t) (minus_SNo (p 0)) HmtR Hm0R Hmt_lt_m0).
We prove the intermediate claim Hmt_q: Rlt (minus_SNo t) q.
An exact proof term for the current goal is (Rlt_tra (minus_SNo t) (minus_SNo (p 0)) q Hmt_m0 Hm0q).
An exact proof term for the current goal is (Hnlt_mt_q Hmt_q).
Assume Heq0: (p 0) = t.
We prove the intermediate claim Hmt_q: Rlt (minus_SNo t) q.
rewrite the current goal using Heq0 (from right to left).
An exact proof term for the current goal is Hm0q.
An exact proof term for the current goal is (Hnlt_mt_q Hmt_q).
Assume Htlt: t < (p 0).
We prove the intermediate claim Hr: Rlt t (p 0).
An exact proof term for the current goal is (RltI t (p 0) HtR Hp0R Htlt).
An exact proof term for the current goal is (FalseE (Hnlt_tx Hr) False).
We use (rectangle_set U0 V0) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbB.
Apply andI to the current goal.
An exact proof term for the current goal is Hpb.
An exact proof term for the current goal is HbSub.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀p0 ∈ U0, ∃b ∈ B, p0 ∈ b ∧ b ⊆ U0) U HUpow HUloc).
We prove the intermediate claim Hex: ∃U0 ∈ Tx, L = X ∖ U0.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUinT.
We will prove L = X ∖ U.
We will prove L = X ∖ (X ∖ L).
Apply set_ext to the current goal.
Let p be given.
Assume HpL: p ∈ L.
We will prove p ∈ X ∖ (X ∖ L).
We prove the intermediate claim HpX: p ∈ X.
An exact proof term for the current goal is (HLsub p HpL).
Apply setminusI X (X ∖ L) p HpX to the current goal.
Assume HpXL: p ∈ X ∖ L.
We prove the intermediate claim HpnotL: p ∉ L.
An exact proof term for the current goal is (setminusE2 X L p HpXL).
An exact proof term for the current goal is (HpnotL HpL).
Let p be given.
Assume Hp: p ∈ X ∖ (X ∖ L).
We will prove p ∈ L.
We prove the intermediate claim HpX: p ∈ X.
An exact proof term for the current goal is (setminusE1 X (X ∖ L) p Hp).
We prove the intermediate claim HpnotXL: p ∉ X ∖ L.
An exact proof term for the current goal is (setminusE2 X (X ∖ L) p Hp).
Apply (xm (p ∈ L)) to the current goal.
Assume HpL: p ∈ L.
An exact proof term for the current goal is HpL.
Assume HpnotL: p ∉ L.
We prove the intermediate claim HpXL: p ∈ X ∖ L.
Apply setminusI to the current goal.
An exact proof term for the current goal is HpX.
An exact proof term for the current goal is HpnotL.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HpnotXL HpXL).
An exact proof term for the current goal is (closed_inI X Tx L HTx HLsub Hex).
∎