Let X, d and N be given.
Assume Hd: metric_on X d.
Assume Hseqc: sequentially_compact X (metric_topology X d).
Assume HNO: N ∈ ω.
We will prove ∃F : set, finite_ball_cover_metric X d (eps_ N) F.
Apply (xm (X = Empty)) to the current goal.
Assume HXEmpty: X = Empty.
We use Empty to witness the existential quantifier.
We will prove finite_ball_cover_metric X d (eps_ N) Empty.
We will prove finite Empty ∧ Empty ⊆ X ∧ X ⊆ (⋃c ∈ Emptyopen_ball X d c (eps_ N)).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is finite_Empty.
Let x be given.
Assume Hx: x ∈ Empty.
We will prove x ∈ X.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x Hx).
rewrite the current goal using HXEmpty (from left to right).
rewrite the current goal using (famunion_Empty (λc0 : set ⇒ open_ball Empty d c0 (eps_ N))) (from left to right).
An exact proof term for the current goal is (Subq_ref Empty).
Assume HXne: ¬ (X = Empty).
Apply (xm (∃F : set, finite_ball_cover_metric X d (eps_ N) F)) to the current goal.
Assume Hex: ∃F : set, finite_ball_cover_metric X d (eps_ N) F.
An exact proof term for the current goal is Hex.
Assume Hno: ¬ (∃F : set, finite_ball_cover_metric X d (eps_ N) F).
We will prove ∃F : set, finite_ball_cover_metric X d (eps_ N) F.
We prove the intermediate claim Hno2: ∀F : set, finite F → F ⊆ X → ¬ (X ⊆ (⋃c ∈ Fopen_ball X d c (eps_ N))).
Let F be given.
Assume HFfin: finite F.
Assume HFsubX: F ⊆ X.
Assume HcovBalls: X ⊆ (⋃c ∈ Fopen_ball X d c (eps_ N)).
Apply Hno to the current goal.
We use F to witness the existential quantifier.
We will prove finite_ball_cover_metric X d (eps_ N) F.
We will prove finite F ∧ F ⊆ X ∧ X ⊆ (⋃c ∈ Fopen_ball X d c (eps_ N)).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HFfin.
An exact proof term for the current goal is HFsubX.
An exact proof term for the current goal is HcovBalls.
We prove the intermediate claim HXne2: X ≠ Empty.
Assume HXeq: X = Empty.
An exact proof term for the current goal is (HXne HXeq).
We prove the intermediate claim Hexx0: ∃x0 : set, x0 ∈ X.
An exact proof term for the current goal is (nonempty_has_element X HXne2).
Apply Hexx0 to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Set BallU to be the term (λF : set ⇒ (⋃c ∈ Fopen_ball X d c (eps_ N))).
Set pick to be the term (λF : set ⇒ Eps_i (λx : set ⇒ x ∈ X ∧ ¬ (x ∈ BallU F))).
We prove the intermediate claim Hpick: ∀F : set, finite F → F ⊆ X → pick F ∈ X ∧ ¬ (pick F ∈ BallU F).
Let F be given.
Assume HFfin: finite F.
Assume HFsubX: F ⊆ X.
We prove the intermediate claim Hnotcov: ¬ (X ⊆ BallU F).
An exact proof term for the current goal is (Hno2 F HFfin HFsubX).
Apply (not_all_ex_demorgan_i (λx : set ⇒ x ∈ X → x ∈ BallU F) Hnotcov) to the current goal.
Let x be given.
Assume HxNotImp: ¬ (x ∈ X → x ∈ BallU F).
We prove the intermediate claim HxX: x ∈ X.
Apply (xm (x ∈ X)) to the current goal.
Assume HxX0: x ∈ X.
An exact proof term for the current goal is HxX0.
Assume HxNotX: ¬ (x ∈ X).
Apply FalseE to the current goal.
Apply HxNotImp to the current goal.
Assume HxX0: x ∈ X.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxNotX HxX0).
We prove the intermediate claim HxNotIn: ¬ (x ∈ BallU F).
Assume HxIn: x ∈ BallU F.
Apply HxNotImp to the current goal.
Assume _: x ∈ X.
An exact proof term for the current goal is HxIn.
We prove the intermediate claim HxPair: x ∈ X ∧ ¬ (x ∈ BallU F).
Apply andI to the current goal.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is HxNotIn.
An exact proof term for the current goal is (Eps_i_ax (λx0 : set ⇒ x0 ∈ X ∧ ¬ (x0 ∈ BallU F)) x HxPair).
Set BaseState to be the term (Empty,x0).
Set StepState to be the term (λn st : set ⇒ ((st 0) ∪ {st 1},pick ((st 0) ∪ {st 1}))).
Set State to be the term (λn : set ⇒ nat_primrec BaseState StepState n).
Set Fof to be the term (λn : set ⇒ (State n) 0).
Set xof to be the term (λn : set ⇒ (State n) 1).
Set Inv to be the term (λst : set ⇒ finite (st 0) ∧ (st 0 ⊆ X) ∧ (st 1 ∈ X) ∧ ¬ (st 1 ∈ BallU (st 0))).
We prove the intermediate claim HInvBase: Inv BaseState.
We will prove finite (BaseState 0) ∧ (BaseState 0 ⊆ X) ∧ (BaseState 1 ∈ X) ∧ ¬ (BaseState 1 ∈ BallU (BaseState 0)).
We prove the intermediate claim HBaseDef: BaseState = (Empty,x0).
Use reflexivity.
rewrite the current goal using HBaseDef (from left to right).
rewrite the current goal using (tuple_2_0_eq Empty x0) (from left to right).
rewrite the current goal using (tuple_2_1_eq Empty x0) (from left to right).
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 finite_Empty.
An exact proof term for the current goal is (Subq_Empty X).
An exact proof term for the current goal is Hx0X.
We prove the intermediate claim HB: BallU Empty = (⋃c ∈ Emptyopen_ball X d c (eps_ N)).
Use reflexivity.
rewrite the current goal using HB (from left to right).
rewrite the current goal using (famunion_Empty (λc : set ⇒ open_ball X d c (eps_ N))) (from left to right).
Assume Hbad: x0 ∈ Empty.
An exact proof term for the current goal is (EmptyE x0 Hbad).
We prove the intermediate claim HInvStep: ∀n st : set, nat_p n → Inv st → Inv (StepState n st).
Let n and st be given.
Assume HnNat: nat_p n.
Assume HInvst: Inv st.
We will prove Inv (StepState n st).
Set Fnew to be the term (st 0) ∪ {st 1}.
Set xnew to be the term pick Fnew.
We prove the intermediate claim HStepDef: StepState n st = (Fnew,xnew).
Use reflexivity.
rewrite the current goal using HStepDef (from left to right).
We will prove finite ((Fnew,xnew) 0) ∧ (((Fnew,xnew) 0) ⊆ X) ∧ ((Fnew,xnew) 1 ∈ X) ∧ ¬ ((Fnew,xnew) 1 ∈ BallU ((Fnew,xnew) 0)).
rewrite the current goal using (tuple_2_0_eq Fnew xnew) (from left to right).
rewrite the current goal using (tuple_2_1_eq Fnew xnew) (from left to right).
We prove the intermediate claim HInvstLeft: (finite (st 0) ∧ (st 0 ⊆ X)) ∧ (st 1 ∈ X).
An exact proof term for the current goal is (andEL ((finite (st 0) ∧ (st 0 ⊆ X)) ∧ (st 1 ∈ X)) (¬ (st 1 ∈ BallU (st 0))) HInvst).
We prove the intermediate claim HFpair: finite (st 0) ∧ (st 0 ⊆ X).
An exact proof term for the current goal is (andEL (finite (st 0) ∧ (st 0 ⊆ X)) (st 1 ∈ X) HInvstLeft).
We prove the intermediate claim Hst1X: st 1 ∈ X.
An exact proof term for the current goal is (andER (finite (st 0) ∧ (st 0 ⊆ X)) (st 1 ∈ X) HInvstLeft).
We prove the intermediate claim HFfin: finite (st 0).
An exact proof term for the current goal is (andEL (finite (st 0)) (st 0 ⊆ X) HFpair).
We prove the intermediate claim HFsubX: st 0 ⊆ X.
An exact proof term for the current goal is (andER (finite (st 0)) (st 0 ⊆ X) HFpair).
We prove the intermediate claim HFnewFin: finite Fnew.
An exact proof term for the current goal is (binunion_finite (st 0) HFfin {st 1} (Sing_finite (st 1))).
We prove the intermediate claim HFnewSubX: Fnew ⊆ X.
Apply (binunion_Subq_min (st 0) {st 1} X HFsubX) to the current goal.
Let y be given.
Assume Hy: y ∈ {st 1}.
We will prove y ∈ X.
rewrite the current goal using (SingE (st 1) y Hy) (from left to right).
An exact proof term for the current goal is Hst1X.
We prove the intermediate claim HpickProp: xnew ∈ X ∧ ¬ (xnew ∈ BallU Fnew).
An exact proof term for the current goal is (Hpick Fnew HFnewFin HFnewSubX).
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 HFnewFin.
An exact proof term for the current goal is HFnewSubX.
An exact proof term for the current goal is (andEL (xnew ∈ X) (¬ (xnew ∈ BallU Fnew)) HpickProp).
An exact proof term for the current goal is (andER (xnew ∈ X) (¬ (xnew ∈ BallU Fnew)) HpickProp).
We prove the intermediate claim HInvAll: ∀n : set, nat_p n → Inv (State n).
Let n be given.
Assume HnNat: nat_p n.
We prove the intermediate claim Hbase: Inv (State 0).
We prove the intermediate claim H0: State 0 = BaseState.
An exact proof term for the current goal is (nat_primrec_0 BaseState StepState).
rewrite the current goal using H0 (from left to right).
An exact proof term for the current goal is HInvBase.
We prove the intermediate claim Hstep: ∀k : set, nat_p k → Inv (State k) → Inv (State (ordsucc k)).
Let k be given.
Assume HkNat: nat_p k.
Assume HInvk: Inv (State k).
We prove the intermediate claim HS: State (ordsucc k) = StepState k (State k).
An exact proof term for the current goal is (nat_primrec_S BaseState StepState k HkNat).
rewrite the current goal using HS (from left to right).
An exact proof term for the current goal is (HInvStep k (State k) HkNat HInvk).
An exact proof term for the current goal is (nat_ind (λt : set ⇒ Inv (State t)) Hbase Hstep n HnNat).
We prove the intermediate claim HFofStep: ∀n : set, nat_p n → (State (ordsucc n)) 0 = ((State n) 0) ∪ {(State n) 1}.
Let n be given.
Assume HnNat: nat_p n.
We prove the intermediate claim HS: State (ordsucc n) = StepState n (State n).
An exact proof term for the current goal is (nat_primrec_S BaseState StepState n HnNat).
rewrite the current goal using HS (from left to right).
We prove the intermediate claim HStepDef: StepState n (State n) = (((State n) 0) ∪ {(State n) 1},pick (((State n) 0) ∪ {(State n) 1})).
Use reflexivity.
rewrite the current goal using HStepDef (from left to right).
rewrite the current goal using (tuple_2_0_eq (((State n) 0) ∪ {(State n) 1}) (pick (((State n) 0) ∪ {(State n) 1}))) (from left to right).
Use reflexivity.
We prove the intermediate claim HMem: ∀n : set, nat_p n → ∀m ∈ n, (State m) 1 ∈ (State n) 0.
Set P to be the term (λn : set ⇒ ∀m ∈ n, (State m) 1 ∈ (State n) 0).
We prove the intermediate claim HP0: P 0.
We will prove ∀m ∈ 0, (State m) 1 ∈ (State 0) 0.
Let m be given.
Assume Hm0: m ∈ 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE m Hm0).
We prove the intermediate claim HPS: ∀n : set, nat_p n → P n → P (ordsucc n).
Let n be given.
Assume HnNat: nat_p n.
Assume IH: ∀m ∈ n, (State m) 1 ∈ (State n) 0.
We will prove ∀m ∈ ordsucc n, (State m) 1 ∈ (State (ordsucc n)) 0.
Let m be given.
Assume HmS: m ∈ ordsucc n.
We prove the intermediate claim HmCase: m ∈ n ∨ m = n.
An exact proof term for the current goal is (ordsuccE n m HmS).
Apply HmCase to the current goal.
Assume Hmn: m ∈ n.
We prove the intermediate claim HmInF: (State m) 1 ∈ (State n) 0.
An exact proof term for the current goal is (IH m Hmn).
rewrite the current goal using (HFofStep n HnNat) (from left to right).
An exact proof term for the current goal is ((binunion_Subq_1 ((State n) 0) {(State n) 1}) ((State m) 1) HmInF).
Assume Hmeq: m = n.
rewrite the current goal using Hmeq (from left to right).
rewrite the current goal using (HFofStep n HnNat) (from left to right).
An exact proof term for the current goal is (binunion_Subq_2 ((State n) 0) {(State n) 1} ((State n) 1) (SingI ((State n) 1))).
Let n be given.
Assume HnNat: nat_p n.
An exact proof term for the current goal is (nat_ind P HP0 HPS n HnNat).
We prove the intermediate claim HSep: ∀n : set, nat_p n → ∀m ∈ n, ¬ ((State n) 1 ∈ open_ball X d ((State m) 1) (eps_ N)).
Let n be given.
Assume HnNat: nat_p n.
Let m be given.
Assume Hmn: m ∈ n.
We prove the intermediate claim HInvn: Inv (State n).
An exact proof term for the current goal is (HInvAll n HnNat).
We prove the intermediate claim HInvn4: ¬ ((State n) 1 ∈ BallU ((State n) 0)).
An exact proof term for the current goal is (andER (((finite ((State n) 0) ∧ ((State n) 0 ⊆ X)) ∧ ((State n) 1 ∈ X))) (¬ ((State n) 1 ∈ BallU ((State n) 0))) HInvn).
We prove the intermediate claim HmInF: (State m) 1 ∈ (State n) 0.
An exact proof term for the current goal is (HMem n HnNat m Hmn).
Assume Hball: (State n) 1 ∈ open_ball X d ((State m) 1) (eps_ N).
Apply HInvn4 to the current goal.
An exact proof term for the current goal is (famunionI ((State n) 0) (λc : set ⇒ open_ball X d c (eps_ N)) ((State m) 1) ((State n) 1) HmInF Hball).
Set seq to be the term graph ω (λn : set ⇒ (State n) 1).
We prove the intermediate claim Hseqval: ∀n : set, n ∈ ω → (State n) 1 ∈ X.
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim HInvn: Inv (State n).
An exact proof term for the current goal is (HInvAll n HnNat).
We prove the intermediate claim HInvnLeft: (finite ((State n) 0) ∧ ((State n) 0 ⊆ X)) ∧ ((State n) 1 ∈ X).
An exact proof term for the current goal is (andEL ((finite ((State n) 0) ∧ ((State n) 0 ⊆ X)) ∧ ((State n) 1 ∈ X)) (¬ ((State n) 1 ∈ BallU ((State n) 0))) HInvn).
An exact proof term for the current goal is (andER (finite ((State n) 0) ∧ ((State n) 0 ⊆ X)) (((State n) 1 ∈ X)) HInvnLeft).
We prove the intermediate claim Htotseq: total_function_on seq ω X.
An exact proof term for the current goal is (total_function_on_graph ω X (λn : set ⇒ (State n) 1) Hseqval).
We prove the intermediate claim Hseq: sequence_on seq X.
An exact proof term for the current goal is (total_function_on_function_on seq ω X Htotseq).
Apply Hseqc to the current goal.
Assume HTx HseqcProp.
Apply (HseqcProp seq Hseq) to the current goal.
Let subseq be given.
Assume Hexsub.
Apply Hexsub to the current goal.
Let x be given.
Assume Hpack.
We prove the intermediate claim Hsubseq: subsequence_of seq subseq.
An exact proof term for the current goal is (andEL (subsequence_of seq subseq) (converges_to X (metric_topology X d) subseq x) Hpack).
We prove the intermediate claim Hconv: converges_to X (metric_topology X d) subseq x.
An exact proof term for the current goal is (andER (subsequence_of seq subseq) (converges_to X (metric_topology X d) subseq x) Hpack).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (converges_to_point_in_X X (metric_topology X d) subseq x Hconv).
We prove the intermediate claim HNnat: nat_p N.
An exact proof term for the current goal is (omega_nat_p N HNO).
Set N1 to be the term ordsucc N.
We prove the intermediate claim HN1omega: N1 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNO).
Set eps1 to be the term eps_ N1.
We prove the intermediate claim Heps1R: eps1 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real eps1 (SNo_eps_SNoS_omega N1 HN1omega)).
We prove the intermediate claim Heps1PosS: 0 < eps1.
An exact proof term for the current goal is (SNo_eps_pos N1 HN1omega).
We prove the intermediate claim Heps1Pos: Rlt 0 eps1.
An exact proof term for the current goal is (RltI 0 eps1 real_0 Heps1R Heps1PosS).
We prove the intermediate claim HepsNR: eps_ N ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N) (SNo_eps_SNoS_omega N HNO)).
We prove the intermediate claim HsumEq: add_SNo eps1 eps1 = eps_ N.
An exact proof term for the current goal is (eps_ordsucc_half_add N HNnat).
We prove the intermediate claim HsumR: add_SNo eps1 eps1 ∈ R.
An exact proof term for the current goal is (real_add_SNo eps1 Heps1R eps1 Heps1R).
Set B1 to be the term open_ball X d x eps1.
We prove the intermediate claim HB1open: B1 ∈ metric_topology X d.
An exact proof term for the current goal is (open_ball_in_metric_topology X d x eps1 Hd HxX Heps1Pos).
We prove the intermediate claim HxB1: x ∈ B1.
An exact proof term for the current goal is (center_in_open_ball X d x eps1 Hd HxX Heps1Pos).
We prove the intermediate claim HexK: ∃K : set, K ∈ ω ∧ ∀n : set, n ∈ ω → K ⊆ n → apply_fun subseq n ∈ B1.
An exact proof term for the current goal is (converges_to_neighborhoods X (metric_topology X d) subseq x Hconv B1 HB1open HxB1).
Apply HexK to the current goal.
Let K be given.
Assume HKpack.
We prove the intermediate claim HKomega: K ∈ ω.
An exact proof term for the current goal is (andEL (K ∈ ω) (∀n : set, n ∈ ω → K ⊆ n → apply_fun subseq n ∈ B1) HKpack).
We prove the intermediate claim Hevent: ∀n : set, n ∈ ω → K ⊆ n → apply_fun subseq n ∈ B1.
An exact proof term for the current goal is (andER (K ∈ ω) (∀n : set, n ∈ ω → K ⊆ n → apply_fun subseq n ∈ B1) HKpack).
Set K2 to be the term ordsucc K.
We prove the intermediate claim HK2omega: K2 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc K HKomega).
We prove the intermediate claim HKsubK2: K ⊆ K2.
An exact proof term for the current goal is (ordsuccI1 K).
We prove the intermediate claim HsubK: apply_fun subseq K ∈ B1.
An exact proof term for the current goal is (Hevent K HKomega (Subq_ref K)).
We prove the intermediate claim HsubK2: apply_fun subseq K2 ∈ B1.
An exact proof term for the current goal is (Hevent K2 HK2omega HKsubK2).
We prove the intermediate claim HKX: apply_fun subseq K ∈ X.
An exact proof term for the current goal is (open_ballE1 X d x eps1 (apply_fun subseq K) HsubK).
We prove the intermediate claim HK2X: apply_fun subseq K2 ∈ X.
An exact proof term for the current goal is (open_ballE1 X d x eps1 (apply_fun subseq K2) HsubK2).
We prove the intermediate claim HdK: Rlt (apply_fun d (x,apply_fun subseq K)) eps1.
An exact proof term for the current goal is (open_ballE2 X d x eps1 (apply_fun subseq K) HsubK).
We prove the intermediate claim HdK2: Rlt (apply_fun d (x,apply_fun subseq K2)) eps1.
An exact proof term for the current goal is (open_ballE2 X d x eps1 (apply_fun subseq K2) HsubK2).
We prove the intermediate claim HdK2sym: Rlt (apply_fun d (apply_fun subseq K2,x)) eps1.
We prove the intermediate claim Hsym: apply_fun d (apply_fun subseq K2,x) = apply_fun d (x,apply_fun subseq K2).
An exact proof term for the current goal is (metric_on_symmetric X d (apply_fun subseq K2) x Hd HK2X HxX).
rewrite the current goal using Hsym (from left to right).
An exact proof term for the current goal is HdK2.
We prove the intermediate claim HfunD: function_on d (setprod X X) R.
An exact proof term for the current goal is (metric_on_function_on X d Hd).
We prove the intermediate claim HdKxR: apply_fun d (x,apply_fun subseq K) ∈ R.
An exact proof term for the current goal is (HfunD (x,apply_fun subseq K) (tuple_2_setprod_by_pair_Sigma X X x (apply_fun subseq K) HxX HKX)).
We prove the intermediate claim HdK2xR: apply_fun d (apply_fun subseq K2,x) ∈ R.
An exact proof term for the current goal is (HfunD (apply_fun subseq K2,x) (tuple_2_setprod_by_pair_Sigma X X (apply_fun subseq K2) x HK2X HxX)).
We prove the intermediate claim HdKK2R: apply_fun d (apply_fun subseq K,apply_fun subseq K2) ∈ R.
An exact proof term for the current goal is (HfunD (apply_fun subseq K,apply_fun subseq K2) (tuple_2_setprod_by_pair_Sigma X X (apply_fun subseq K) (apply_fun subseq K2) HKX HK2X)).
We prove the intermediate claim HdKxS: SNo (apply_fun d (x,apply_fun subseq K)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x,apply_fun subseq K)) HdKxR).
We prove the intermediate claim HdK2xS: SNo (apply_fun d (apply_fun subseq K2,x)).
An exact proof term for the current goal is (real_SNo (apply_fun d (apply_fun subseq K2,x)) HdK2xR).
We prove the intermediate claim Heps1S: SNo eps1.
An exact proof term for the current goal is (real_SNo eps1 Heps1R).
We prove the intermediate claim HdKxLt: apply_fun d (x,apply_fun subseq K) < eps1.
An exact proof term for the current goal is (RltE_lt (apply_fun d (x,apply_fun subseq K)) eps1 HdK).
We prove the intermediate claim HdK2xLt: apply_fun d (apply_fun subseq K2,x) < eps1.
An exact proof term for the current goal is (RltE_lt (apply_fun d (apply_fun subseq K2,x)) eps1 HdK2sym).
We prove the intermediate claim Htmp1S: add_SNo (apply_fun d (x,apply_fun subseq K)) (apply_fun d (apply_fun subseq K2,x)) < add_SNo (apply_fun d (x,apply_fun subseq K)) eps1.
An exact proof term for the current goal is (add_SNo_Lt2 (apply_fun d (x,apply_fun subseq K)) (apply_fun d (apply_fun subseq K2,x)) eps1 HdKxS HdK2xS Heps1S HdK2xLt).
We prove the intermediate claim Htmp1R: Rlt (add_SNo (apply_fun d (x,apply_fun subseq K)) (apply_fun d (apply_fun subseq K2,x))) (add_SNo (apply_fun d (x,apply_fun subseq K)) eps1).
An exact proof term for the current goal is (RltI (add_SNo (apply_fun d (x,apply_fun subseq K)) (apply_fun d (apply_fun subseq K2,x))) (add_SNo (apply_fun d (x,apply_fun subseq K)) eps1) (real_add_SNo (apply_fun d (x,apply_fun subseq K)) HdKxR (apply_fun d (apply_fun subseq K2,x)) HdK2xR) (real_add_SNo (apply_fun d (x,apply_fun subseq K)) HdKxR eps1 Heps1R) Htmp1S).
We prove the intermediate claim Htmp2S: add_SNo (apply_fun d (x,apply_fun subseq K)) eps1 < add_SNo eps1 eps1.
An exact proof term for the current goal is (add_SNo_Lt1 (apply_fun d (x,apply_fun subseq K)) eps1 eps1 HdKxS Heps1S Heps1S HdKxLt).
We prove the intermediate claim Htmp2R: Rlt (add_SNo (apply_fun d (x,apply_fun subseq K)) eps1) (add_SNo eps1 eps1).
An exact proof term for the current goal is (RltI (add_SNo (apply_fun d (x,apply_fun subseq K)) eps1) (add_SNo eps1 eps1) (real_add_SNo (apply_fun d (x,apply_fun subseq K)) HdKxR eps1 Heps1R) (real_add_SNo eps1 Heps1R eps1 Heps1R) Htmp2S).
We prove the intermediate claim HsumRlt_eps: Rlt (add_SNo (apply_fun d (x,apply_fun subseq K)) (apply_fun d (apply_fun subseq K2,x))) (add_SNo eps1 eps1).
An exact proof term for the current goal is (Rlt_tra (add_SNo (apply_fun d (x,apply_fun subseq K)) (apply_fun d (apply_fun subseq K2,x))) (add_SNo (apply_fun d (x,apply_fun subseq K)) eps1) (add_SNo eps1 eps1) Htmp1R Htmp2R).
We prove the intermediate claim HsumRlt: Rlt (add_SNo (apply_fun d (x,apply_fun subseq K)) (apply_fun d (apply_fun subseq K2,x))) (eps_ N).
rewrite the current goal using HsumEq (from right to left).
An exact proof term for the current goal is HsumRlt_eps.
We prove the intermediate claim HtriNot: ¬ (Rlt (add_SNo (apply_fun d (apply_fun subseq K,x)) (apply_fun d (x,apply_fun subseq K2))) (apply_fun d (apply_fun subseq K,apply_fun subseq K2))).
An exact proof term for the current goal is (metric_on_triangle X d (apply_fun subseq K) x (apply_fun subseq K2) Hd HKX HxX HK2X).
We prove the intermediate claim Hsym1: apply_fun d (apply_fun subseq K,x) = apply_fun d (x,apply_fun subseq K).
An exact proof term for the current goal is (metric_on_symmetric X d (apply_fun subseq K) x Hd HKX HxX).
We prove the intermediate claim Hsym2: apply_fun d (x,apply_fun subseq K2) = apply_fun d (apply_fun subseq K2,x).
An exact proof term for the current goal is (metric_on_symmetric X d x (apply_fun subseq K2) Hd HxX HK2X).
We prove the intermediate claim HsumRlt2: Rlt (add_SNo (apply_fun d (apply_fun subseq K,x)) (apply_fun d (x,apply_fun subseq K2))) (eps_ N).
rewrite the current goal using Hsym1 (from left to right) at position 1.
rewrite the current goal using Hsym2 (from left to right) at position 1.
An exact proof term for the current goal is HsumRlt.
We prove the intermediate claim Htri: Rle (apply_fun d (apply_fun subseq K,apply_fun subseq K2)) (add_SNo (apply_fun d (apply_fun subseq K,x)) (apply_fun d (x,apply_fun subseq K2))).
Apply (RleI (apply_fun d (apply_fun subseq K,apply_fun subseq K2)) (add_SNo (apply_fun d (apply_fun subseq K,x)) (apply_fun d (x,apply_fun subseq K2))) HdKK2R (real_add_SNo (apply_fun d (apply_fun subseq K,x)) (HfunD (apply_fun subseq K,x) (tuple_2_setprod_by_pair_Sigma X X (apply_fun subseq K) x HKX HxX)) (apply_fun d (x,apply_fun subseq K2)) (HfunD (x,apply_fun subseq K2) (tuple_2_setprod_by_pair_Sigma X X x (apply_fun subseq K2) HxX HK2X)))) to the current goal.
Assume Hbad: Rlt (add_SNo (apply_fun d (apply_fun subseq K,x)) (apply_fun d (x,apply_fun subseq K2))) (apply_fun d (apply_fun subseq K,apply_fun subseq K2)).
An exact proof term for the current goal is (HtriNot Hbad).
We prove the intermediate claim HdKK2Lt: Rlt (apply_fun d (apply_fun subseq K,apply_fun subseq K2)) (eps_ N).
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid (apply_fun d (apply_fun subseq K,apply_fun subseq K2)) (add_SNo (apply_fun d (apply_fun subseq K,x)) (apply_fun d (x,apply_fun subseq K2))) (eps_ N) Htri HsumRlt2).
Apply Hsubseq to the current goal.
Let f be given.
Assume Hfpack.
We prove the intermediate claim Hsubeq: subseq = compose_fun ω f seq.
An exact proof term for the current goal is (andER (((total_function_on f ω ω ∧ functional_graph f) ∧ graph_domain_subset f ω) ∧ omega_strictly_increasing f) (subseq = compose_fun ω f seq) Hfpack).
We prove the intermediate claim Hfcore: ((total_function_on f ω ω ∧ functional_graph f) ∧ graph_domain_subset f ω) ∧ omega_strictly_increasing f.
An exact proof term for the current goal is (andEL (((total_function_on f ω ω ∧ functional_graph f) ∧ graph_domain_subset f ω) ∧ omega_strictly_increasing f) (subseq = compose_fun ω f seq) Hfpack).
We prove the intermediate claim Hfcore2: (total_function_on f ω ω ∧ functional_graph f) ∧ graph_domain_subset f ω.
An exact proof term for the current goal is (andEL ((total_function_on f ω ω ∧ functional_graph f) ∧ graph_domain_subset f ω) (omega_strictly_increasing f) Hfcore).
We prove the intermediate claim Hfinc: omega_strictly_increasing f.
An exact proof term for the current goal is (andER ((total_function_on f ω ω ∧ functional_graph f) ∧ graph_domain_subset f ω) (omega_strictly_increasing f) Hfcore).
We prove the intermediate claim Hfcore3: total_function_on f ω ω ∧ functional_graph f.
An exact proof term for the current goal is (andEL (total_function_on f ω ω ∧ functional_graph f) (graph_domain_subset f ω) Hfcore2).
We prove the intermediate claim Hftot: total_function_on f ω ω.
An exact proof term for the current goal is (andEL (total_function_on f ω ω) (functional_graph f) Hfcore3).
We prove the intermediate claim HKinK2: K ∈ K2.
An exact proof term for the current goal is (ordsuccI2 K).
We prove the intermediate claim HfKO: apply_fun f K ∈ ω.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y f ω ω K Hftot HKomega).
We prove the intermediate claim HfK2O: apply_fun f K2 ∈ ω.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y f ω ω K2 Hftot HK2omega).
We prove the intermediate claim HfKIn: apply_fun f K ∈ apply_fun f K2.
An exact proof term for the current goal is (Hfinc K K2 HKomega HK2omega HKinK2).
We prove the intermediate claim HsubKdef: apply_fun subseq K = apply_fun seq (apply_fun f K).
rewrite the current goal using Hsubeq (from left to right).
An exact proof term for the current goal is (compose_fun_apply ω f seq K HKomega).
We prove the intermediate claim HsubK2def: apply_fun subseq K2 = apply_fun seq (apply_fun f K2).
rewrite the current goal using Hsubeq (from left to right).
An exact proof term for the current goal is (compose_fun_apply ω f seq K2 HK2omega).
We prove the intermediate claim HdXofLt: Rlt (apply_fun d (xof (apply_fun f K),xof (apply_fun f K2))) (eps_ N).
We prove the intermediate claim HseqFK: apply_fun seq (apply_fun f K) = xof (apply_fun f K).
rewrite the current goal using (apply_fun_graph ω (λn : set ⇒ (State n) 1) (apply_fun f K) HfKO) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HseqFK2: apply_fun seq (apply_fun f K2) = xof (apply_fun f K2).
rewrite the current goal using (apply_fun_graph ω (λn : set ⇒ (State n) 1) (apply_fun f K2) HfK2O) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HseqFK (from right to left) at position 1.
rewrite the current goal using HseqFK2 (from right to left) at position 1.
rewrite the current goal using HsubKdef (from right to left) at position 1.
rewrite the current goal using HsubK2def (from right to left) at position 1.
An exact proof term for the current goal is HdKK2Lt.
We prove the intermediate claim HxK2InBall: xof (apply_fun f K2) ∈ open_ball X d (xof (apply_fun f K)) (eps_ N).
We prove the intermediate claim HxK2X: xof (apply_fun f K2) ∈ X.
An exact proof term for the current goal is (Hseqval (apply_fun f K2) HfK2O).
We prove the intermediate claim Hdlt: Rlt (apply_fun d (xof (apply_fun f K),xof (apply_fun f K2))) (eps_ N).
An exact proof term for the current goal is HdXofLt.
An exact proof term for the current goal is (open_ballI X d (xof (apply_fun f K)) (eps_ N) (xof (apply_fun f K2)) HxK2X Hdlt).
We prove the intermediate claim HsepContra: ¬ (xof (apply_fun f K2) ∈ open_ball X d (xof (apply_fun f K)) (eps_ N)).
An exact proof term for the current goal is (HSep (apply_fun f K2) (omega_nat_p (apply_fun f K2) HfK2O) (apply_fun f K) HfKIn).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HsepContra HxK2InBall).
∎