We will prove ¬ finer_than R_lower_limit_topology R_K_topology ∧ ¬ finer_than R_K_topology R_lower_limit_topology.
Apply andI to the current goal.
Assume Hf: finer_than R_lower_limit_topology R_K_topology.
We will prove False.
Set U to be the term open_interval (minus_SNo 1) 1 ∖ K_set.
We prove the intermediate claim HUm1R: minus_SNo 1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim HU1R: 1 ∈ R.
An exact proof term for the current goal is real_1.
We prove the intermediate claim HUinKbasis: U ∈ R_K_basis.
We will prove U ∈ R_K_basis.
Apply (famunionI R (λa0 : set ⇒ {open_interval a0 b ∖ K_set|b ∈ R}) (minus_SNo 1) U HUm1R) to the current goal.
We prove the intermediate claim HUfam: U ∈ {open_interval (minus_SNo 1) b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (ReplI R (λb0 : set ⇒ open_interval (minus_SNo 1) b0 ∖ K_set) 1 HU1R).
An exact proof term for the current goal is HUfam.
We prove the intermediate claim HUinB: U ∈ (R_standard_basis ∪ R_K_basis).
An exact proof term for the current goal is (binunionI2 R_standard_basis R_K_basis U HUinKbasis).
We prove the intermediate claim HUinKtop: U ∈ R_K_topology.
An exact proof term for the current goal is (basis_in_generated R (R_standard_basis ∪ R_K_basis) U R_standard_plus_K_basis_is_basis_local HUinB).
We prove the intermediate claim HUinLower: U ∈ R_lower_limit_topology.
An exact proof term for the current goal is (Hf U HUinKtop).
We prove the intermediate claim H0inU: 0 ∈ U.
We will prove 0 ∈ U.
Apply setminusI to the current goal.
We will prove 0 ∈ open_interval (minus_SNo 1) 1.
We prove the intermediate claim Hm10: Rlt (minus_SNo 1) 0.
Apply RltI to the current goal.
An exact proof term for the current goal is HUm1R.
An exact proof term for the current goal is real_0.
An exact proof term for the current goal is minus_1_lt_0.
We prove the intermediate claim H01: Rlt 0 1.
An exact proof term for the current goal is Rlt_0_1.
We prove the intermediate claim H0prop: Rlt (minus_SNo 1) 0 ∧ Rlt 0 1.
An exact proof term for the current goal is (andI (Rlt (minus_SNo 1) 0) (Rlt 0 1) Hm10 H01).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) 0 real_0 H0prop).
An exact proof term for the current goal is zero_not_in_K_set.
We prove the intermediate claim HUcond: ∀x ∈ U, ∃b ∈ R_lower_limit_basis, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_lower_limit_basis, x0 ∈ b0 ∧ b0 ⊆ U0) U HUinLower).
We prove the intermediate claim Hexb0: ∃b0 ∈ R_lower_limit_basis, 0 ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (HUcond 0 H0inU).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0pair: b0 ∈ R_lower_limit_basis ∧ (0 ∈ b0 ∧ b0 ⊆ U).
We prove the intermediate claim Hb0inB: b0 ∈ R_lower_limit_basis.
An exact proof term for the current goal is (andEL (b0 ∈ R_lower_limit_basis) (0 ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hb0rest: 0 ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (andER (b0 ∈ R_lower_limit_basis) (0 ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim H0inb0: 0 ∈ b0.
An exact proof term for the current goal is (andEL (0 ∈ b0) (b0 ⊆ U) Hb0rest).
We prove the intermediate claim Hb0subU: b0 ⊆ U.
An exact proof term for the current goal is (andER (0 ∈ b0) (b0 ⊆ U) Hb0rest).
We prove the intermediate claim Hexa0: ∃a0 ∈ R, b0 ∈ {halfopen_interval_left a0 b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {halfopen_interval_left a0 b|b ∈ R}) b0 Hb0inB).
Apply Hexa0 to the current goal.
Let a0 be given.
Assume Ha0pair: a0 ∈ R ∧ b0 ∈ {halfopen_interval_left a0 b|b ∈ R}.
We prove the intermediate claim Ha0R: a0 ∈ R.
An exact proof term for the current goal is (andEL (a0 ∈ R) (b0 ∈ {halfopen_interval_left a0 b|b ∈ R}) Ha0pair).
We prove the intermediate claim Hb0fam: b0 ∈ {halfopen_interval_left a0 b|b ∈ R}.
An exact proof term for the current goal is (andER (a0 ∈ R) (b0 ∈ {halfopen_interval_left a0 b|b ∈ R}) Ha0pair).
We prove the intermediate claim Hexb1: ∃b1 ∈ R, b0 = halfopen_interval_left a0 b1.
An exact proof term for the current goal is (ReplE R (λb1 : set ⇒ halfopen_interval_left a0 b1) b0 Hb0fam).
Apply Hexb1 to the current goal.
Let b1 be given.
Assume Hb1pair: b1 ∈ R ∧ b0 = halfopen_interval_left a0 b1.
We prove the intermediate claim Hb1R: b1 ∈ R.
An exact proof term for the current goal is (andEL (b1 ∈ R) (b0 = halfopen_interval_left a0 b1) Hb1pair).
We prove the intermediate claim Hb0eq: b0 = halfopen_interval_left a0 b1.
An exact proof term for the current goal is (andER (b1 ∈ R) (b0 = halfopen_interval_left a0 b1) Hb1pair).
We prove the intermediate claim H0inHalf: 0 ∈ halfopen_interval_left a0 b1.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is H0inb0.
We prove the intermediate claim H0prop: ¬ (Rlt 0 a0) ∧ Rlt 0 b1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 a0) ∧ Rlt x0 b1) 0 H0inHalf).
We prove the intermediate claim Hnot0lta0: ¬ (Rlt 0 a0).
An exact proof term for the current goal is (andEL (¬ (Rlt 0 a0)) (Rlt 0 b1) H0prop).
We prove the intermediate claim H0ltb1: Rlt 0 b1.
An exact proof term for the current goal is (andER (¬ (Rlt 0 a0)) (Rlt 0 b1) H0prop).
We prove the intermediate claim Hexy: ∃y : set, y ∈ b0 ∧ y ∈ K_set.
We prove the intermediate claim Hexy2: ∃y : set, y ∈ halfopen_interval_left a0 b1 ∧ y ∈ K_set.
An exact proof term for the current goal is (K_set_meets_lower_limit_neighborhood_0 a0 b1 Ha0R Hb1R Hnot0lta0 H0ltb1).
Apply Hexy2 to the current goal.
Let y be given.
Assume Hyconj2: y ∈ halfopen_interval_left a0 b1 ∧ y ∈ K_set.
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is (andEL (y ∈ halfopen_interval_left a0 b1) (y ∈ K_set) Hyconj2).
An exact proof term for the current goal is (andER (y ∈ halfopen_interval_left a0 b1) (y ∈ K_set) Hyconj2).
Apply Hexy to the current goal.
Let y be given.
Assume Hyconj: y ∈ b0 ∧ y ∈ K_set.
We prove the intermediate claim Hyb0: y ∈ b0.
An exact proof term for the current goal is (andEL (y ∈ b0) (y ∈ K_set) Hyconj).
We prove the intermediate claim HyK: y ∈ K_set.
An exact proof term for the current goal is (andER (y ∈ b0) (y ∈ K_set) Hyconj).
We prove the intermediate claim HyinU: y ∈ U.
An exact proof term for the current goal is (Hb0subU y Hyb0).
We prove the intermediate claim HynotK: y ∉ K_set.
An exact proof term for the current goal is (setminusE2 (open_interval (minus_SNo 1) 1) K_set y HyinU).
An exact proof term for the current goal is (HynotK HyK).
Assume Hf: finer_than R_K_topology R_lower_limit_topology.
We will prove False.
Set U0 to be the term halfopen_interval_left 0 1.
We prove the intermediate claim HU0Lower: U0 ∈ R_lower_limit_topology.
We will prove U0 ∈ R_lower_limit_topology.
We will prove U0 ∈ generated_topology R R_lower_limit_basis.
We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 R.
An exact proof term for the current goal is (PowerI R U0 (halfopen_interval_left_Subq_R 0 1)).
We prove the intermediate claim HU0Prop: ∀x ∈ U0, ∃b0 ∈ R_lower_limit_basis, x ∈ b0 ∧ b0 ⊆ U0.
Let x be given.
Assume HxU0: x ∈ U0.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ Rlt x0 1) x HxU0).
We prove the intermediate claim HxProp: ¬ (Rlt x 0) ∧ Rlt x 1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ Rlt x0 1) x HxU0).
We prove the intermediate claim Hxlt1: Rlt x 1.
An exact proof term for the current goal is (andER (¬ (Rlt x 0)) (Rlt x 1) HxProp).
Set bx to be the term halfopen_interval_left x 1.
We use bx to witness the existential quantifier.
Apply andI to the current goal.
We will prove bx ∈ R_lower_limit_basis.
Apply (famunionI R (λa0 : set ⇒ {halfopen_interval_left a0 b|b ∈ R}) x bx HxR) to the current goal.
An exact proof term for the current goal is (ReplI R (λb0 : set ⇒ halfopen_interval_left x b0) 1 real_1).
Apply andI to the current goal.
We will prove x ∈ bx.
We prove the intermediate claim Hnotxx: ¬ (Rlt x x).
An exact proof term for the current goal is (not_Rlt_refl x HxR).
We prove the intermediate claim Hxpropbx: ¬ (Rlt x x) ∧ Rlt x 1.
An exact proof term for the current goal is (andI (¬ (Rlt x x)) (Rlt x 1) Hnotxx Hxlt1).
An exact proof term for the current goal is (SepI R (λt : set ⇒ ¬ (Rlt t x) ∧ Rlt t 1) x HxR Hxpropbx).
We will prove bx ⊆ U0.
Let y be given.
Assume Hybx: y ∈ bx.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t x) ∧ Rlt t 1) y Hybx).
We prove the intermediate claim HyProp: ¬ (Rlt y x) ∧ Rlt y 1.
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t x) ∧ Rlt t 1) y Hybx).
We prove the intermediate claim Hylt1: Rlt y 1.
An exact proof term for the current goal is (andER (¬ (Rlt y x)) (Rlt y 1) HyProp).
We prove the intermediate claim Hnotyltx: ¬ (Rlt y x).
An exact proof term for the current goal is (andEL (¬ (Rlt y x)) (Rlt y 1) HyProp).
We prove the intermediate claim Hnotxlt0: ¬ (x < 0).
Assume Hxlt0: x < 0.
We prove the intermediate claim HxRlt0: Rlt x 0.
An exact proof term for the current goal is (RltI x 0 HxR real_0 Hxlt0).
An exact proof term for the current goal is ((andEL (¬ (Rlt x 0)) (Rlt x 1) HxProp) HxRlt0).
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 H0S: SNo 0.
An exact proof term for the current goal is SNo_0.
We prove the intermediate claim HxLe0or: x < 0 ∨ 0 ≤ x.
An exact proof term for the current goal is (SNoLtLe_or x 0 HxS H0S).
We prove the intermediate claim H0Lex: 0 ≤ x.
Apply (HxLe0or (0 ≤ x)) to the current goal.
Assume Hxlt0: x < 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnotxlt0 Hxlt0).
Assume H.
An exact proof term for the current goal is H.
We prove the intermediate claim Hnotylt0: ¬ (Rlt y 0).
Assume Hylt0: Rlt y 0.
We prove the intermediate claim Hylt0lt: y < 0.
An exact proof term for the current goal is (RltE_lt y 0 Hylt0).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim Hyltx: y < x.
An exact proof term for the current goal is (SNoLtLe_tra y 0 x HyS H0S HxS Hylt0lt H0Lex).
We prove the intermediate claim HyRltx: Rlt y x.
An exact proof term for the current goal is (RltI y x HyR HxR Hyltx).
An exact proof term for the current goal is (Hnotyltx HyRltx).
We prove the intermediate claim HyPropU0: ¬ (Rlt y 0) ∧ Rlt y 1.
An exact proof term for the current goal is (andI (¬ (Rlt y 0)) (Rlt y 1) Hnotylt0 Hylt1).
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z 0) ∧ Rlt z 1) y HyR HyPropU0).
An exact proof term for the current goal is (SepI (𝒫 R) (λU : set ⇒ ∀x ∈ U, ∃b0 ∈ R_lower_limit_basis, x ∈ b0 ∧ b0 ⊆ U) U0 HU0Pow HU0Prop).
We prove the intermediate claim HU0K: U0 ∈ R_K_topology.
An exact proof term for the current goal is (Hf U0 HU0Lower).
We prove the intermediate claim H0inU0: 0 ∈ U0.
We will prove 0 ∈ U0.
We prove the intermediate claim Hnot00: ¬ (Rlt 0 0).
An exact proof term for the current goal is (not_Rlt_refl 0 real_0).
We prove the intermediate claim H0prop: ¬ (Rlt 0 0) ∧ Rlt 0 1.
An exact proof term for the current goal is (andI (¬ (Rlt 0 0)) (Rlt 0 1) Hnot00 Rlt_0_1).
An exact proof term for the current goal is (SepI R (λz : set ⇒ ¬ (Rlt z 0) ∧ Rlt z 1) 0 real_0 H0prop).
We prove the intermediate claim HU0cond: ∀x ∈ U0, ∃b1 ∈ (R_standard_basis ∪ R_K_basis), x ∈ b1 ∧ b1 ⊆ U0.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU : set ⇒ ∀x0 ∈ U, ∃b1 ∈ (R_standard_basis ∪ R_K_basis), x0 ∈ b1 ∧ b1 ⊆ U) U0 HU0K).
We prove the intermediate claim Hexb1: ∃b1 ∈ (R_standard_basis ∪ R_K_basis), 0 ∈ b1 ∧ b1 ⊆ U0.
An exact proof term for the current goal is (HU0cond 0 H0inU0).
Apply Hexb1 to the current goal.
Let b1 be given.
Assume Hb1pair.
We prove the intermediate claim Hb1B: b1 ∈ (R_standard_basis ∪ R_K_basis).
An exact proof term for the current goal is (andEL (b1 ∈ (R_standard_basis ∪ R_K_basis)) (0 ∈ b1 ∧ b1 ⊆ U0) Hb1pair).
We prove the intermediate claim Hb1rest: 0 ∈ b1 ∧ b1 ⊆ U0.
An exact proof term for the current goal is (andER (b1 ∈ (R_standard_basis ∪ R_K_basis)) (0 ∈ b1 ∧ b1 ⊆ U0) Hb1pair).
We prove the intermediate claim H0inb1: 0 ∈ b1.
An exact proof term for the current goal is (andEL (0 ∈ b1) (b1 ⊆ U0) Hb1rest).
We prove the intermediate claim Hb1subU0: b1 ⊆ U0.
An exact proof term for the current goal is (andER (0 ∈ b1) (b1 ⊆ U0) Hb1rest).
Apply (binunionE R_standard_basis R_K_basis b1 Hb1B) to the current goal.
Assume Hb1Std: b1 ∈ R_standard_basis.
We prove the intermediate claim Hexa: ∃a ∈ R, b1 ∈ {open_interval a b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) b1 Hb1Std).
Apply Hexa to the current goal.
Let a0 be given.
Assume Ha0pair.
We prove the intermediate claim Ha0R: a0 ∈ R.
An exact proof term for the current goal is (andEL (a0 ∈ R) (b1 ∈ {open_interval a0 b|b ∈ R}) Ha0pair).
We prove the intermediate claim Hb1Fam: b1 ∈ {open_interval a0 b|b ∈ R}.
An exact proof term for the current goal is (andER (a0 ∈ R) (b1 ∈ {open_interval a0 b|b ∈ R}) Ha0pair).
We prove the intermediate claim Hexc: ∃c0 ∈ R, b1 = open_interval a0 c0.
An exact proof term for the current goal is (ReplE R (λc : set ⇒ open_interval a0 c) b1 Hb1Fam).
Apply Hexc to the current goal.
Let c0 be given.
Assume Hc0pair.
We prove the intermediate claim Hc0R: c0 ∈ R.
An exact proof term for the current goal is (andEL (c0 ∈ R) (b1 = open_interval a0 c0) Hc0pair).
We prove the intermediate claim Hb1eq: b1 = open_interval a0 c0.
An exact proof term for the current goal is (andER (c0 ∈ R) (b1 = open_interval a0 c0) Hc0pair).
We prove the intermediate claim H0inInt: 0 ∈ open_interval a0 c0.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is H0inb1.
We prove the intermediate claim H0IntProp: Rlt a0 0 ∧ Rlt 0 c0.
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ Rlt a0 t ∧ Rlt t c0) 0 H0inInt).
We prove the intermediate claim Ha0lt0: Rlt a0 0.
An exact proof term for the current goal is (andEL (Rlt a0 0) (Rlt 0 c0) H0IntProp).
We prove the intermediate claim H0ltc0: Rlt 0 c0.
An exact proof term for the current goal is (andER (Rlt a0 0) (Rlt 0 c0) H0IntProp).
Set e1 to be the term eps_ 1.
We prove the intermediate claim H1omega: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim He1SNoS: e1 ∈ SNoS_ ω.
An exact proof term for the current goal is (SNo_eps_SNoS_omega 1 H1omega).
We prove the intermediate claim He1R: e1 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real e1 He1SNoS).
We prove the intermediate claim He1S: SNo e1.
An exact proof term for the current goal is (real_SNo e1 He1R).
We prove the intermediate claim He1pos: 0 < e1.
An exact proof term for the current goal is (SNo_eps_pos 1 H1omega).
We prove the intermediate claim H0Ord: ordinal 0.
An exact proof term for the current goal is (nat_p_ordinal 0 nat_0).
We prove the intermediate claim H0in1: 0 ∈ 1.
An exact proof term for the current goal is (ordinal_0_In_ordsucc 0 H0Ord).
We prove the intermediate claim He1lt1: e1 < 1.
We prove the intermediate claim He1ltE0: eps_ 1 < eps_ 0.
An exact proof term for the current goal is (SNo_eps_decr 1 H1omega 0 H0in1).
rewrite the current goal using (eps_0_1) (from right to left) at position 2.
An exact proof term for the current goal is He1ltE0.
Set y to be the term mul_SNo a0 e1.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (real_mul_SNo a0 Ha0R e1 He1R).
We prove the intermediate claim Ha0S: SNo a0.
An exact proof term for the current goal is (real_SNo a0 Ha0R).
We prove the intermediate claim HyNeg: y < 0.
An exact proof term for the current goal is (mul_SNo_neg_pos a0 e1 Ha0S He1S (RltE_lt a0 0 Ha0lt0) He1pos).
We prove the intermediate claim Hyltc0: y < c0.
We prove the intermediate claim H0ltc0lt: 0 < c0.
An exact proof term for the current goal is (RltE_lt 0 c0 H0ltc0).
We prove the intermediate claim Hc0S: SNo c0.
An exact proof term for the current goal is (real_SNo c0 Hc0R).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
An exact proof term for the current goal is (SNoLt_tra y 0 c0 HyS SNo_0 Hc0S HyNeg H0ltc0lt).
We prove the intermediate claim Ha0lty: a0 < y.
We prove the intermediate claim Ha0lt: a0 < 0.
An exact proof term for the current goal is (RltE_lt a0 0 Ha0lt0).
We prove the intermediate claim Ha0mul: mul_SNo a0 1 < mul_SNo a0 e1.
An exact proof term for the current goal is (neg_mul_SNo_Lt a0 1 e1 Ha0S Ha0lt SNo_1 He1S He1lt1).
We will prove a0 < y.
rewrite the current goal using (mul_SNo_oneR a0 Ha0S) (from right to left) at position 1.
An exact proof term for the current goal is Ha0mul.
We prove the intermediate claim HyInt: y ∈ open_interval a0 c0.
We will prove y ∈ open_interval a0 c0.
We prove the intermediate claim Harlt: Rlt a0 y.
An exact proof term for the current goal is (RltI a0 y Ha0R HyR Ha0lty).
We prove the intermediate claim Hyrc0: Rlt y c0.
An exact proof term for the current goal is (RltI y c0 HyR Hc0R Hyltc0).
We prove the intermediate claim Hconj: Rlt a0 y ∧ Rlt y c0.
An exact proof term for the current goal is (andI (Rlt a0 y) (Rlt y c0) Harlt Hyrc0).
An exact proof term for the current goal is (SepI R (λt : set ⇒ Rlt a0 t ∧ Rlt t c0) y HyR Hconj).
We prove the intermediate claim Hyinb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is HyInt.
We prove the intermediate claim HyinU0: y ∈ U0.
An exact proof term for the current goal is (Hb1subU0 y Hyinb1).
We prove the intermediate claim HyU0prop: ¬ (Rlt y 0) ∧ Rlt y 1.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z 0) ∧ Rlt z 1) y HyinU0).
We prove the intermediate claim Hnotylt0: ¬ (Rlt y 0).
An exact proof term for the current goal is (andEL (¬ (Rlt y 0)) (Rlt y 1) HyU0prop).
We prove the intermediate claim HyRlt0: Rlt y 0.
An exact proof term for the current goal is (RltI y 0 HyR real_0 HyNeg).
An exact proof term for the current goal is (Hnotylt0 HyRlt0).
Assume Hb1K: b1 ∈ R_K_basis.
We prove the intermediate claim Hexa: ∃a ∈ R, b1 ∈ {open_interval a b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b ∖ K_set|b ∈ R}) b1 Hb1K).
Apply Hexa to the current goal.
Let a0 be given.
Assume Ha0pair.
We prove the intermediate claim Ha0R: a0 ∈ R.
An exact proof term for the current goal is (andEL (a0 ∈ R) (b1 ∈ {open_interval a0 b ∖ K_set|b ∈ R}) Ha0pair).
We prove the intermediate claim Hb1Fam: b1 ∈ {open_interval a0 b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (andER (a0 ∈ R) (b1 ∈ {open_interval a0 b ∖ K_set|b ∈ R}) Ha0pair).
We prove the intermediate claim Hexc: ∃c0 ∈ R, b1 = open_interval a0 c0 ∖ K_set.
An exact proof term for the current goal is (ReplE R (λc : set ⇒ open_interval a0 c ∖ K_set) b1 Hb1Fam).
Apply Hexc to the current goal.
Let c0 be given.
Assume Hc0pair.
We prove the intermediate claim Hc0R: c0 ∈ R.
An exact proof term for the current goal is (andEL (c0 ∈ R) (b1 = open_interval a0 c0 ∖ K_set) Hc0pair).
We prove the intermediate claim Hb1eq: b1 = open_interval a0 c0 ∖ K_set.
An exact proof term for the current goal is (andER (c0 ∈ R) (b1 = open_interval a0 c0 ∖ K_set) Hc0pair).
We prove the intermediate claim H0inSetminus: 0 ∈ open_interval a0 c0 ∖ K_set.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is H0inb1.
We prove the intermediate claim H0inInt: 0 ∈ open_interval a0 c0.
An exact proof term for the current goal is (setminusE1 (open_interval a0 c0) K_set 0 H0inSetminus).
We prove the intermediate claim H0IntProp: Rlt a0 0 ∧ Rlt 0 c0.
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ Rlt a0 t ∧ Rlt t c0) 0 H0inInt).
We prove the intermediate claim Ha0lt0: Rlt a0 0.
An exact proof term for the current goal is (andEL (Rlt a0 0) (Rlt 0 c0) H0IntProp).
We prove the intermediate claim H0ltc0: Rlt 0 c0.
An exact proof term for the current goal is (andER (Rlt a0 0) (Rlt 0 c0) H0IntProp).
Set e1 to be the term eps_ 1.
We prove the intermediate claim H1omega: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim He1SNoS: e1 ∈ SNoS_ ω.
An exact proof term for the current goal is (SNo_eps_SNoS_omega 1 H1omega).
We prove the intermediate claim He1R: e1 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real e1 He1SNoS).
We prove the intermediate claim He1S: SNo e1.
An exact proof term for the current goal is (real_SNo e1 He1R).
We prove the intermediate claim He1pos: 0 < e1.
An exact proof term for the current goal is (SNo_eps_pos 1 H1omega).
We prove the intermediate claim H0Ord: ordinal 0.
An exact proof term for the current goal is (nat_p_ordinal 0 nat_0).
We prove the intermediate claim H0in1: 0 ∈ 1.
An exact proof term for the current goal is (ordinal_0_In_ordsucc 0 H0Ord).
We prove the intermediate claim He1lt1: e1 < 1.
We prove the intermediate claim He1ltE0: eps_ 1 < eps_ 0.
An exact proof term for the current goal is (SNo_eps_decr 1 H1omega 0 H0in1).
rewrite the current goal using (eps_0_1) (from right to left) at position 2.
An exact proof term for the current goal is He1ltE0.
Set y to be the term mul_SNo a0 e1.
We prove the intermediate claim Ha0S: SNo a0.
An exact proof term for the current goal is (real_SNo a0 Ha0R).
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (real_mul_SNo a0 Ha0R e1 He1R).
We prove the intermediate claim HyNeg: y < 0.
An exact proof term for the current goal is (mul_SNo_neg_pos a0 e1 Ha0S He1S (RltE_lt a0 0 Ha0lt0) He1pos).
We prove the intermediate claim Hyltc0: y < c0.
We prove the intermediate claim H0ltc0lt: 0 < c0.
An exact proof term for the current goal is (RltE_lt 0 c0 H0ltc0).
We prove the intermediate claim Hc0S: SNo c0.
An exact proof term for the current goal is (real_SNo c0 Hc0R).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
An exact proof term for the current goal is (SNoLt_tra y 0 c0 HyS SNo_0 Hc0S HyNeg H0ltc0lt).
We prove the intermediate claim Ha0lty: a0 < y.
We prove the intermediate claim Ha0lt: a0 < 0.
An exact proof term for the current goal is (RltE_lt a0 0 Ha0lt0).
We prove the intermediate claim Ha0mul: mul_SNo a0 1 < mul_SNo a0 e1.
An exact proof term for the current goal is (neg_mul_SNo_Lt a0 1 e1 Ha0S Ha0lt SNo_1 He1S He1lt1).
We will prove a0 < y.
rewrite the current goal using (mul_SNo_oneR a0 Ha0S) (from right to left) at position 1.
An exact proof term for the current goal is Ha0mul.
We prove the intermediate claim HyInt: y ∈ open_interval a0 c0.
We will prove y ∈ open_interval a0 c0.
We prove the intermediate claim Harlt: Rlt a0 y.
An exact proof term for the current goal is (RltI a0 y Ha0R HyR Ha0lty).
We prove the intermediate claim Hyrc0: Rlt y c0.
An exact proof term for the current goal is (RltI y c0 HyR Hc0R Hyltc0).
We prove the intermediate claim Hconj: Rlt a0 y ∧ Rlt y c0.
An exact proof term for the current goal is (andI (Rlt a0 y) (Rlt y c0) Harlt Hyrc0).
An exact proof term for the current goal is (SepI R (λt : set ⇒ Rlt a0 t ∧ Rlt t c0) y HyR Hconj).
We prove the intermediate claim HynotK: y ∉ K_set.
Assume HyK: y ∈ K_set.
Apply (ReplE_impred (ω ∖ {0}) (λm : set ⇒ inv_nat m) y HyK False) to the current goal.
Let m be given.
Assume HmIn: m ∈ ω ∖ {0}.
Assume Hyeq: y = inv_nat m.
We prove the intermediate claim Hypos: Rlt 0 y.
rewrite the current goal using Hyeq (from left to right).
An exact proof term for the current goal is (inv_nat_pos m HmIn).
We prove the intermediate claim Hyposlt: 0 < y.
An exact proof term for the current goal is (RltE_lt 0 y Hypos).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim H0lt0: 0 < 0.
An exact proof term for the current goal is (SNoLt_tra 0 y 0 SNo_0 HyS SNo_0 Hyposlt HyNeg).
An exact proof term for the current goal is ((SNoLt_irref 0) H0lt0).
We prove the intermediate claim HyinSetminus: y ∈ open_interval a0 c0 ∖ K_set.
An exact proof term for the current goal is (setminusI (open_interval a0 c0) K_set y HyInt HynotK).
We prove the intermediate claim Hyinb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is HyinSetminus.
We prove the intermediate claim HyinU0: y ∈ U0.
An exact proof term for the current goal is (Hb1subU0 y Hyinb1).
We prove the intermediate claim HyU0prop: ¬ (Rlt y 0) ∧ Rlt y 1.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z 0) ∧ Rlt z 1) y HyinU0).
We prove the intermediate claim Hnotylt0: ¬ (Rlt y 0).
An exact proof term for the current goal is (andEL (¬ (Rlt y 0)) (Rlt y 1) HyU0prop).
We prove the intermediate claim HyRlt0: Rlt y 0.
An exact proof term for the current goal is (RltI y 0 HyR real_0 HyNeg).
An exact proof term for the current goal is (Hnotylt0 HyRlt0).
∎