(**
This file is part of the Coquelicot formalization of real
analysis in Coq: http://coquelicot.saclay.inria.fr/

Copyright (C) 2011-2015 Sylvie Boldo
#<br />#
Copyright (C) 2011-2015 Catherine Lelay
#<br />#
Copyright (C) 2011-2015 Guillaume Melquiond

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

Require Import Reals Psatz.
Require Import mathcomp.ssreflect.ssreflect Rbar.
Require Import Rcomplements.
Require Import Lim_seq Continuity Derive Series.
Require Import Lub Hierarchy.

(** This file describes sequences of functions and results about
their convergence. *)

Open Scope R_scope.

(** * Sequence of functions *)

(** ** Definitions *)

Definition CVS_dom (fn : nat -> R -> R) (D : R -> Prop) :=
  forall x : R, D x -> ex_finite_lim_seq (fun n => fn n x).

Definition CVU_dom (fn : nat -> R -> R) (D : R -> Prop) :=
  forall eps : posreal, eventually (fun n => forall x : R,
    D x -> Rabs ((fn n x) - real (Lim_seq (fun n => fn n x))) < eps).
Definition CVU_cauchy (fn : nat -> R -> R) (D : R -> Prop) :=
  forall eps : posreal, exists N : nat,
  forall (n m : nat) (x : R), D x -> (N <= n)%nat -> (N <= m)%nat
    -> Rabs (fn n x - fn m x) < eps.

(** Equivalence with standard library *)

Lemma CVU_dom_Reals (fn : nat -> R -> R) (f : R -> R) (x : R) (r : posreal) :
  (forall y, (Boule x r y) -> (Finite (f y)) = Lim_seq (fun n => fn n y)) ->
  (CVU fn f x r <-> CVU_dom fn (Boule x r)).
Proof.
(* Goal: forall _ : forall (y : R) (_ : Boule x r y), @eq Rbar (Finite (f y)) (Lim_seq (fun n : nat => fn n y)), iff (CVU fn f x r) (CVU_dom fn (Boule x r)) *)
  split ; move => Hcvu.
(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
  have Hf : forall y, Boule x r y -> is_lim_seq (fun n => fn n y) (f y).
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move => y Hy.
(* Goal: is_lim_seq (fun n : nat => fn n x) (Finite (real (Lim_seq (fun n : nat => fn n x)))) *)
    apply is_lim_seq_spec.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move => [e He] /=.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (Hcvu e He) => {Hcvu} N Hcvu.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    exists N => n Hn.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite -Ropp_minus_distr' Rabs_Ropp.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Hcvu.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move => [e He] /=.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (Hcvu e He) => {Hcvu} N Hcvu.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  exists N => n Hn y Hy.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite (is_lim_seq_unique (fun n0 : nat => fn n0 y) _ (Hf y Hy)).
(* Goal: Rlt (Rabs (Rminus (fn n y) (real (Finite (f y))))) e *)
(* Goal: CVU fn f x r *)
  simpl.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite -/(Rminus (fn n y) (f y)) -Ropp_minus_distr' Rabs_Ropp.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply Hcvu.

(* Goal: CVU fn f x r *)
  move => e He ; set eps := mkposreal e He.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (Hcvu eps) => {Hcvu} N Hcvu.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  exists N => n y Hn Hy.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move: (Hcvu n Hn y Hy).
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite -(H y Hy) /=.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  by rewrite -Ropp_minus_distr' Rabs_Ropp.
Qed.

(** Various inclusions and equivalences between definitions *)

Lemma CVU_CVS_dom (fn : nat -> R -> R) (D : R -> Prop) :
  CVU_dom fn D -> CVS_dom fn D.
Proof.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move => Hcvu x Hx.
(* Goal: ex_finite_lim_seq (fun n : nat => fn n x) *)
  exists (real (Lim_seq (fun n => fn n x))).
(* Goal: is_lim_seq (fun n : nat => fn n x) (Finite (real (Lim_seq (fun n : nat => fn n x)))) *)
  apply is_lim_seq_spec.
(* Goal: is_lim' (fn n) (Finite x) (Finite (fn n x)) *)
(* Goal: continuity_pt (fun y : R => real (Lim_seq (fun n : nat => fn n y))) x *)
  intros eps.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (Hcvu eps) => {Hcvu} N Hcvu.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  exists N => n Hn.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply Hcvu.
Qed.
Lemma CVU_dom_cauchy (fn : nat -> R -> R) (D : R -> Prop) :
  CVU_dom fn D <-> CVU_cauchy fn D.
Proof.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  split => H eps.
(* CVU_dom -> CVU_cauchy *)
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (H (pos_div_2 eps)) => {H} N /= H.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  exists N => n m x Hx Hn Hm.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite (double_var eps).
  replace (fn n x - fn m x)
    with ((fn n x - real (Lim_seq (fun n0 : nat => fn n0 x)))
      - (fn m x - real (Lim_seq (fun n0 : nat => fn n0 x))))
(* Goal: @eq R (Rminus (Rplus (sum_f_R0 An n) (Series (fun k : nat => An (S (Init.Nat.add n k))))) (sum_f_R0 An n)) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule An *)
(* Goal: is_lim_seq (fun n : nat => Rminus (Series An) (sum_f_R0 An n)) (Finite (IZR Z0)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    by ring.
(* Goal: Rlt (Rabs (Rminus (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x)))) (Rminus (fn m x) (real (Lim_seq (fun n0 : nat => fn n0 x)))))) (Rplus (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) *)
(* Goal: eventually (fun n : nat => forall (x : R) (_ : D x), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (pos eps)) *)
  apply Rle_lt_trans with (1 := Rabs_triang _ _) ; rewrite Rabs_Ropp.
(* Goal: Rlt (Rplus (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rabs (Rminus (fn m x) (real (Lim_seq (fun n0 : nat => fn n0 x)))))) (Rplus (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) *)
(* Goal: eventually (fun n : nat => forall (x : R) (_ : D x), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (pos eps)) *)
  apply Rplus_lt_compat ; by apply H.
(* CVU_cauchy -> CVU_dom *)
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite /Lim_seq.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (H (pos_div_2 eps)) => {H} N /= H.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  exists N => n Hn x Hx.
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus (Finite ls) (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  rewrite /LimSup_seq ; case: ex_LimSup_seq ; case => [ls | | ] /= Hls.
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus (Finite ls) (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  rewrite /LimInf_seq ; case: ex_LimInf_seq ; case => [li | | ] /= Hli.
  replace (fn n x - (ls + li) / 2)
    with (((fn n x - ls) + (fn n x - li))/2)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by field.
(* Goal: Rlt (Rdiv (Rabs (Rplus (Rminus (fn n x) ls) (Rminus (fn n x) li))) (IZR (Zpos (xO xH)))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  rewrite Rabs_div ; [ | by apply Rgt_not_eq, Rlt_R0_R2].
(* Goal: Rlt (Rdiv (Rabs (Rplus (Rminus (fn n x) ls) (Rminus (fn n x) li))) (IZR (Zpos (xO xH)))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  rewrite (Rabs_pos_eq 2) ; [ | by apply Rlt_le, Rlt_R0_R2].
(* Goal: Rlt (Rdiv (Rabs (Rplus (Rminus (fn n x) ls) (Rminus (fn n x) li))) (IZR (Zpos (xO xH)))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  rewrite Rlt_div_l ; [ | by apply Rlt_R0_R2].
(* Goal: Rlt (Rabs (Rminus (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ (S i)))) (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i))))) (Rplus (pos eps) (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (pos eps) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_lt_trans with (1 := Rabs_triang _ _).
(* Goal: Rlt (Rplus (Rabs (Rminus (fn n x) ls)) (Rabs (Rminus (fn n x) li))) (Rmult (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  replace (eps * 2) with (eps + eps) by ring.
(* Goal: Rlt (Rplus (Rabs (Rminus (fn n x) ls)) (Rabs (Rminus (fn n x) li))) (Rplus (pos eps) (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  apply Rplus_lt_compat ; apply Rabs_lt_between'.
(* Goal: and (Rlt (Rminus li (pos eps)) (fn n x)) (Rlt (fn n x) (Rplus li (pos eps))) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  case: (Hls (pos_div_2 eps)) => {Hls Hli} /= H0 [N0 H1] ; split.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (H0 N) => {H0} m [Hm H0].
(* Goal: Rlt (Rminus ls (pos eps)) (fn n x) *)
(* Goal: Rlt (fn n x) (Rplus ls (pos eps)) *)
(* Goal: and (Rlt (Rminus li (pos eps)) (fn n x)) (Rlt (fn n x) (Rplus li (pos eps))) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  apply Rlt_trans with (fn m x - eps/2).
  replace (ls - eps)
    with ((ls - eps / 2) - eps/2)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by field.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply Rplus_lt_compat_r.
(* Goal: Rlt (Rminus (fn (Init.Nat.add n N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) (fn n x) *)
(* Goal: Rlt (fn n x) (Rplus li (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  replace (fn n x) with (eps/2 + (fn n x - eps/2)) by ring.
(* Goal: Rlt (Rminus (fn m x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) (Rplus (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rminus (fn n x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) *)
(* Goal: Rlt (fn n x) (Rplus ls (pos eps)) *)
(* Goal: and (Rlt (Rminus li (pos eps)) (fn n x)) (Rlt (fn n x) (Rplus li (pos eps))) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  replace (fn m x - eps / 2) with ((fn m x - fn n x) + (fn n x - eps/2)) by ring.
(* Goal: Rlt (Rplus (Rminus (fn n x) (fn (Init.Nat.add N N0) x)) (Rminus (fn (Init.Nat.add N N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) (Rplus (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rminus (fn (Init.Nat.add N N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) *)
  apply Rplus_lt_compat_r.
(* Goal: Rlt (Rminus (fn n x) (fn m x)) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (Rplus (fn m x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) (Rplus li (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  apply Rle_lt_trans with (1 := Rle_abs _) ; by apply H.
(* Goal: Rlt (fn n x) (Rplus ls (pos eps)) *)
(* Goal: and (Rlt (Rminus li (pos eps)) (fn n x)) (Rlt (fn n x) (Rplus li (pos eps))) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  apply Rlt_trans with (fn (n+N0)%nat x + eps/2).
(* Goal: Rlt (fn n x) (Rplus (fn (Init.Nat.add n N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rplus (fn (Init.Nat.add n N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) (Rplus ls (pos eps)) *)
(* Goal: and (Rlt (Rminus li (pos eps)) (fn n x)) (Rlt (fn n x) (Rplus li (pos eps))) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  replace (fn n x) with (fn (n + N0)%nat x + (fn n x - fn (n+N0)%nat x)) by ring.
(* Goal: Rlt (Rplus (fn n x) (Rminus (fn (Init.Nat.add N N0) x) (fn n x))) (Rplus (fn n x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  apply Rplus_lt_compat_l.
(* Goal: Rlt (Rplus (Rminus (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ (S i)))) (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i)))) (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (Rplus (Rplus (pos eps) (pos eps)) (pos eps)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_lt_trans with (1 := Rle_abs _).
(* Goal: Rlt (Rabs (Rminus (fn n x) (fn (Init.Nat.add N N0) x))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
  apply H ; by intuition.
(* Goal: Rlt (Rplus (fn (Init.Nat.add n N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) (Rplus ls (pos eps)) *)
(* Goal: and (Rlt (Rminus li (pos eps)) (fn n x)) (Rlt (fn n x) (Rplus li (pos eps))) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  replace (ls + eps) with ((ls + eps/2) + eps/2) by field.
(* Goal: Rlt (Rplus (Rminus (fn n x) (fn (Init.Nat.add N N0) x)) (Rminus (fn (Init.Nat.add N N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) (Rplus (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rminus (fn (Init.Nat.add N N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) *)
  apply Rplus_lt_compat_r.
(* Goal: Rlt (Rminus li (Rdiv (pos eps) (IZR (Zpos (xO xH))))) (fn (Init.Nat.add n N0) x) *)
(* Goal: Rlt (Rminus (fn (Init.Nat.add n N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) (fn n x) *)
(* Goal: Rlt (fn n x) (Rplus li (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  apply H1 ; by intuition.
(* Goal: and (Rlt (Rminus li (pos eps)) (fn n x)) (Rlt (fn n x) (Rplus li (pos eps))) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  case: (Hli (pos_div_2 eps)) => {Hls Hli} /= H0 [N0 H1] ; split.
(* Goal: Rlt (Rminus li (pos eps)) (fn n x) *)
(* Goal: Rlt (fn n x) (Rplus li (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  apply Rlt_trans with (fn (n+N0)%nat x - eps/2).
(* Goal: Rlt (Rminus li (pos eps)) (Rminus (fn (Init.Nat.add n N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rminus (fn (Init.Nat.add n N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) (fn n x) *)
(* Goal: Rlt (fn n x) (Rplus li (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  replace (li - eps) with ((li - eps/2) - eps/2) by field.
(* Goal: Rlt (Rplus (Rminus (fn n x) (fn (Init.Nat.add N N0) x)) (Rminus (fn (Init.Nat.add N N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) (Rplus (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rminus (fn (Init.Nat.add N N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) *)
  apply Rplus_lt_compat_r.
(* Goal: Rlt (Rminus li (Rdiv (pos eps) (IZR (Zpos (xO xH))))) (fn (Init.Nat.add n N0) x) *)
(* Goal: Rlt (Rminus (fn (Init.Nat.add n N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) (fn n x) *)
(* Goal: Rlt (fn n x) (Rplus li (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  apply H1 ; by intuition.
(* Goal: Rlt (Rminus (fn (Init.Nat.add n N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) (fn n x) *)
(* Goal: Rlt (fn n x) (Rplus li (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  replace (fn n x) with (eps/2 + (fn n x - eps/2)) by ring.
  replace (fn (n + N0)%nat x - eps / 2)
    with ((fn (n + N0)%nat x - fn n x) + (fn n x - eps/2))
(* Goal: @eq R (Rminus (Rplus (sum_f_R0 An n) (Series (fun k : nat => An (S (Init.Nat.add n k))))) (sum_f_R0 An n)) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule An *)
(* Goal: is_lim_seq (fun n : nat => Rminus (Series An) (sum_f_R0 An n)) (Finite (IZR Z0)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    by ring.
(* Goal: Rlt (Rplus (Rminus (fn n x) (fn (Init.Nat.add N N0) x)) (Rminus (fn (Init.Nat.add N N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) (Rplus (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rminus (fn (Init.Nat.add N N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) *)
  apply Rplus_lt_compat_r.
(* Goal: Rlt (Rplus (Rminus (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ (S i)))) (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i)))) (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (Rplus (Rplus (pos eps) (pos eps)) (pos eps)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_lt_trans with (1 := Rle_abs _).
(* Goal: Rlt (Rabs (Rminus (fn n x) (fn (Init.Nat.add N N0) x))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
  apply H ; by intuition.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (H0 N) => {H0} m [Hm H0].
(* Goal: Rlt (fn n x) (Rplus li (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  apply Rlt_trans with (fn m x + eps/2).
(* Goal: Rlt (fn n x) (Rplus (fn m x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rplus (fn m x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) (Rplus li (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  replace (fn n x) with (fn m x + (fn n x - fn m x)) by ring.
(* Goal: Rlt (Rplus (fn n x) (Rminus (fn (Init.Nat.add N N0) x) (fn n x))) (Rplus (fn n x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  apply Rplus_lt_compat_l.
(* Goal: Rlt (Rminus (fn n x) (fn m x)) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (Rplus (fn m x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) (Rplus li (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  apply Rle_lt_trans with (1 := Rle_abs _) ; by apply H.
  replace (li + eps)
    with ((li + eps / 2) + eps/2)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by field.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply Rplus_lt_compat_r.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (Hli (fn n x + eps / 2)) => {Hls Hli} N0 H0.
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  move: (H0 _ (le_plus_r N N0)) => {H0} H0 ; contradict H0.
(* Goal: not (Rlt (fn (Init.Nat.add N N0) x) (Rminus (fn n x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) *)
  apply Rle_not_lt, Rlt_le.
  replace (fn (N + N0)%nat x)
    with (fn n x + (fn (N + N0)%nat x - fn n x))
(* Goal: @eq R (Rminus (Rplus (sum_f_R0 An n) (Series (fun k : nat => An (S (Init.Nat.add n k))))) (sum_f_R0 An n)) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule An *)
(* Goal: is_lim_seq (fun n : nat => Rminus (Series An) (sum_f_R0 An n)) (Finite (IZR Z0)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    by ring.
(* Goal: Rlt (Rplus (fn n x) (Rminus (fn (Init.Nat.add N N0) x) (fn n x))) (Rplus (fn n x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (IZR Z0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  apply Rplus_lt_compat_l.
(* Goal: Rlt (Rplus (Rminus (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ (S i)))) (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i)))) (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (Rplus (Rplus (pos eps) (pos eps)) (pos eps)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_lt_trans with (1 := Rle_abs _).
(* Goal: Rlt (Rabs (Rminus (fn n x) (fn (Init.Nat.add N N0) x))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
  apply H ; by intuition.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (Hli (fn n x - eps / 2) N) => {Hls Hli} m [Hm H0].
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  contradict H0.
(* Goal: not (Rlt (fn (Init.Nat.add N N0) x) (Rminus (fn n x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) *)
  apply Rle_not_lt, Rlt_le.
(* Goal: Rlt (Rminus (fn n x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) (fn m x) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  replace (fn m x) with (eps/2 + (fn m x - eps/2)) by ring.
  replace (fn n x - eps / 2)
(* Goal: @eq R (Rminus (Rplus (sum_f_R0 An n) (Series (fun k : nat => An (S (Init.Nat.add n k))))) (sum_f_R0 An n)) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule An *)
(* Goal: is_lim_seq (fun n : nat => Rminus (Series An) (sum_f_R0 An n)) (Finite (IZR Z0)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    with ((fn n x - fn m x) + (fn m x - eps/2)) by ring.
(* Goal: Rlt (Rplus (Rminus (fn n x) (fn m x)) (Rminus (fn m x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) (Rplus (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rminus (fn m x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  apply Rplus_lt_compat_r, Rle_lt_trans with (1 := Rle_abs _) ; by apply H.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (Hls (fn n x + eps / 2) N) => {Hls} m [Hm H0].
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus p_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  contradict H0.
(* Goal: not (Rlt (fn (Init.Nat.add N N0) x) (Rminus (fn n x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) *)
  apply Rle_not_lt, Rlt_le.
(* Goal: Rlt (fn m x) (Rplus (fn n x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  replace (fn m x) with (fn n x + (fn m x - fn n x)) by ring.
(* Goal: Rlt (Rplus (fn n x) (Rminus (fn m x) (fn n x))) (Rplus (fn n x) (Rdiv (pos eps) (IZR (Zpos (xO xH))))) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  apply Rplus_lt_compat_l, Rle_lt_trans with (1 := Rle_abs _) ; by apply H.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (Hls (fn n x - eps / 2)) => {Hls} N0 H0.
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Rbar_div_pos (Rbar_plus m_infty (LimInf_seq (fun n : nat => fn n x))) (mkposreal (IZR (Zpos (xO xH))) Rlt_R0_R2))))) (pos eps) *)
  move: (H0 _ (le_plus_r N N0)) => {H0} H0 ; contradict H0.
(* Goal: not (Rlt (fn (Init.Nat.add N N0) x) (Rminus (fn n x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) *)
  apply Rle_not_lt, Rlt_le.
  replace (fn (N + N0)%nat x)
    with (eps/2 + (fn (N + N0)%nat x - eps/2))
(* Goal: @eq R (Rminus (Rplus (sum_f_R0 An n) (Series (fun k : nat => An (S (Init.Nat.add n k))))) (sum_f_R0 An n)) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule An *)
(* Goal: is_lim_seq (fun n : nat => Rminus (Series An) (sum_f_R0 An n)) (Finite (IZR Z0)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    by ring.
  replace (fn n x - eps / 2)
(* Goal: @eq R (Rminus (Rplus (sum_f_R0 An n) (Series (fun k : nat => An (S (Init.Nat.add n k))))) (sum_f_R0 An n)) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule An *)
(* Goal: is_lim_seq (fun n : nat => Rminus (Series An) (sum_f_R0 An n)) (Finite (IZR Z0)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    with ((fn n x - fn (N+N0)%nat x) + (fn (N+N0)%nat x - eps/2)) by ring.
(* Goal: Rlt (Rplus (Rminus (fn n x) (fn (Init.Nat.add N N0) x)) (Rminus (fn (Init.Nat.add N N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) (Rplus (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rminus (fn (Init.Nat.add N N0) x) (Rdiv (pos eps) (IZR (Zpos (xO xH)))))) *)
  apply Rplus_lt_compat_r.
(* Goal: Rlt (Rplus (Rminus (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ (S i)))) (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i)))) (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (Rplus (Rplus (pos eps) (pos eps)) (pos eps)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_lt_trans with (1 := Rle_abs _).
(* Goal: Rlt (Rabs (Rminus (fn n x) (fn (Init.Nat.add N N0) x))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
  apply H ; by intuition.
Qed.

Lemma CVU_dom_include (fn : nat -> R -> R) (D1 D2 : R -> Prop) :
  (forall y, D2 y -> D1 y) -> CVU_dom fn D1 -> CVU_dom fn D2.
Proof.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move => H H1 eps.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (H1 eps) => {H1} N H1.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  exists N => n Hn x Hx.
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n : nat => fn n x))))) (pos eps) *)
  apply H1.
(* Goal: le N n *)
(* Goal: D1 x *)
  exact Hn.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply H.
Qed.

(** ** Limits, integrals and differentiability *)

Definition is_connected (D : R -> Prop) :=
  forall a b x, D a -> D b -> a <= x <= b -> D x.

Lemma CVU_limits_open (fn : nat -> R -> R) (D : R -> Prop) :
  open D
  -> CVU_dom fn D
  -> (forall x n, D x -> ex_finite_lim (fn n) x)
  -> forall x, D x -> ex_finite_lim_seq (fun n => real (Lim (fn n) x))
    /\ ex_finite_lim (fun y => real (Lim_seq (fun n => fn n y))) x
    /\ real (Lim_seq (fun n => real (Lim (fn n) x)))
      = real (Lim (fun y => real (Lim_seq (fun n => fn n y))) x).
Proof.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move => Ho Hfn Hex x Hx.
(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
  have H : ex_finite_lim_seq (fun n : nat => real (Lim (fn n) x)).
(* Goal: ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    apply CVU_dom_cauchy in Hfn.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    apply ex_lim_seq_cauchy_corr => eps.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (Hfn (pos_div_2 eps)) => {Hfn} /= N Hfn.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    exists N => n m Hn Hm.
    case: (Hex x n Hx) => ln Hex_n ;
    rewrite (is_lim_unique _ _ _ Hex_n).
    case: (Hex x m Hx) => {Hex} lm Hex_m ;
    rewrite (is_lim_unique _ _ _ Hex_m).
(* Goal: Rlt (Rabs (Rminus (real (Finite ln)) (real (Finite lm)))) (pos eps) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    apply is_lim_spec in Hex_n.
(* Goal: Rlt (Rabs (Rminus (real (Finite ln)) (real (Finite lm)))) (pos eps) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    apply is_lim_spec in Hex_m.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (Hex_n (pos_div_2 (pos_div_2 eps))) => {Hex_n} /= dn Hex_n.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (Hex_m (pos_div_2 (pos_div_2 eps))) => {Hex_m} /= dm Hex_m.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (Ho x Hx) => {Ho} d0 Ho.
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    set y := x + Rmin (Rmin dn dm) d0 / 2.
(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
    have Hd : 0 < Rmin (Rmin dn dm) d0 / 2.
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (IZR (Zpos (xI (xO xH))))) *)
(* Goal: forall eps : posreal, @ex nat (fun N : nat => forall (n : nat) (_ : le N n) (x : R) (_ : AB x), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps))) *)
      apply Rdiv_lt_0_compat.
(* Goal: Rlt (IZR Z0) (Rmin (Rmin (pos dn) (pos dm)) (pos d0)) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
(* Goal: Rlt (Rabs (Rminus ln lm)) (pos eps) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
      apply Rmin_case ; [ | by apply d0].
(* Goal: Rlt (IZR Z0) (Rmin (pos d0) (pos d1)) *)
(* Goal: @locally' R_UniformSpace x (fun y : R => Rlt (Rabs (Rminus (real (Lim_seq (fun n : nat => fn n y))) l)) (pos eps)) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
      apply Rmin_case ; [ by apply dn | by apply dm].
(* Goal: Rlt (dist R_met y x) d *)
      exact: Rlt_R0_R2.
(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
    have Hy : Rabs (y - x) < d0.
(* Goal: Rlt (Rabs (Rminus y x)) (pos d0) *)
(* Goal: Rlt (Rabs (Rminus ln lm)) (pos eps) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
      rewrite /y ; ring_simplify ((x + Rmin (Rmin dn dm) d0 / 2) - x).
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
      rewrite (Rabs_pos_eq _ (Rlt_le _ _ Hd)).
(* Goal: Rlt (Rdiv (Rmin (Rmin (pos dn) (pos dm)) (pos d0)) (IZR (Zpos (xO xH)))) (pos d0) *)
(* Goal: Rlt (Rabs (Rminus ln lm)) (pos eps) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
      generalize (Rmin_r (Rmin dn dm) d0).
(* Goal: forall (_ : Rle (Rmin (Rmin (pos dn) (pos dm)) (pos d0)) (Rmin (pos dn) (pos dm))) (_ : Rle (Rmin (pos dn) (pos dm)) (pos dm)), Rlt (Rdiv (Rmin (Rmin (pos dn) (pos dm)) (pos d0)) (IZR (Zpos (xO xH)))) (pos dm) *)
(* Goal: not (@eq R y x) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn m y))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
      lra.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move : (Ho y Hy) => {Ho Hy} Hy.
    replace (ln - lm)
      with (- (fn n y - ln) + (fn m y - lm) + (fn n y - fn m y))
(* Goal: @eq R (Rminus (Rplus (sum_f_R0 An n) (Series (fun k : nat => An (S (Init.Nat.add n k))))) (sum_f_R0 An n)) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule An *)
(* Goal: is_lim_seq (fun n : nat => Rminus (Series An) (sum_f_R0 An n)) (Finite (IZR Z0)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
      by ring.
    rewrite (double_var eps) ;
    apply Rle_lt_trans with (1 := Rabs_triang _ _), Rplus_lt_compat.
    rewrite (double_var (eps/2)) ;
    apply Rle_lt_trans with (1 := Rabs_triang _ _), Rplus_lt_compat.
(* Goal: Rlt (Rabs (Ropp (Rminus (fn n y) ln))) (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (Rabs (Rminus (fn m y) lm)) (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn m y))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    rewrite Rabs_Ropp ; apply Hex_n.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite /y /ball /= /AbsRing_ball /= /minus /plus /opp /abs /=.
(* Goal: Rlt (Rabs (Rplus (Rplus x (Rdiv (Rmin (Rmin (pos dn) (pos dm)) (pos d0)) (IZR (Zpos (xO xH))))) (Ropp x))) (pos dm) *)
(* Goal: not (@eq R y x) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn m y))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    ring_simplify ((x + Rmin (Rmin dn dm) d0 / 2) + - x).
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite (Rabs_pos_eq _ (Rlt_le _ _ Hd)).
(* Goal: Rlt (Rdiv (Rmin (Rmin (pos dn) (pos dm)) (pos d0)) (IZR (Zpos (xO xH)))) (pos dn) *)
(* Goal: not (@eq R y x) *)
(* Goal: Rlt (Rabs (Rminus (fn m y) lm)) (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn m y))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    generalize (Rmin_l (Rmin dn dm) d0) (Rmin_l dn dm).
(* Goal: forall (_ : Rle (Rmin (Rmin (pos dn) (pos dm)) (pos d0)) (Rmin (pos dn) (pos dm))) (_ : Rle (Rmin (pos dn) (pos dm)) (pos dm)), Rlt (Rdiv (Rmin (Rmin (pos dn) (pos dm)) (pos d0)) (IZR (Zpos (xO xH)))) (pos dm) *)
(* Goal: not (@eq R y x) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn m y))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    lra.
(* Goal: not (@eq R y x) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn m y))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    apply Rgt_not_eq, Rlt_gt, Rminus_lt_0.
(* Goal: Rlt (IZR Z0) (Rminus y x) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn m y))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    rewrite /y ; by ring_simplify ((x + Rmin (Rmin dn dm) d0 / 2) - x).
(* Goal: Rlt (Rabs (Rminus (fn m y) lm)) (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn m y))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    apply Hex_m.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite /y /ball /= /AbsRing_ball /= /minus /plus /opp /abs /=.
(* Goal: Rlt (Rabs (Rplus (Rplus x (Rdiv (Rmin (Rmin (pos dn) (pos dm)) (pos d0)) (IZR (Zpos (xO xH))))) (Ropp x))) (pos dm) *)
(* Goal: not (@eq R y x) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn m y))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    ring_simplify ((x + Rmin (Rmin dn dm) d0 / 2) + - x).
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite (Rabs_pos_eq _ (Rlt_le _ _ Hd)).
(* Goal: Rlt (Rdiv (Rmin (Rmin (pos dn) (pos dm)) (pos d0)) (IZR (Zpos (xO xH)))) (pos dm) *)
(* Goal: not (@eq R y x) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn m y))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    generalize (Rmin_l (Rmin dn dm) d0) (Rmin_r dn dm).
(* Goal: forall (_ : Rle (Rmin (Rmin (pos dn) (pos dm)) (pos d0)) (Rmin (pos dn) (pos dm))) (_ : Rle (Rmin (pos dn) (pos dm)) (pos dm)), Rlt (Rdiv (Rmin (Rmin (pos dn) (pos dm)) (pos d0)) (IZR (Zpos (xO xH)))) (pos dm) *)
(* Goal: not (@eq R y x) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn m y))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    lra.
(* Goal: not (@eq R y x) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn m y))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    apply Rgt_not_eq, Rlt_gt, Rminus_lt_0.
(* Goal: Rlt (IZR Z0) (Rminus y x) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn m y))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    rewrite /y ; by ring_simplify ((x + Rmin (Rmin dn dm) d0 / 2) - x).
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Hfn.
(* Goal: D_x no_cond x y *)
(* Goal: Rlt (dist R_met y x) d *)
  split.
(* Goal: Rlt (dist R_met y x) d *)
  exact: H.
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
  apply Lim_seq_correct' in H.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move: (real (Lim_seq (fun n : nat => real (Lim (fn n) x)))) H => l H.
(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
  have H0 : is_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) x l.
(* Goal: is_lim (fn n) (Finite x) (Finite (fn n x)) *)
    apply is_lim_spec.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move => eps.
(* Goal: Rbar_locally' (Finite x) (fun y : R => Rlt (Rabs (Rminus (real (Lim_seq (fun n : nat => fn n y))) l)) (pos eps)) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
    apply is_lim_seq_spec in H.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (Hfn (pos_div_2 (pos_div_2 eps))) => {Hfn} /= n1 Hfn.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (H (pos_div_2 (pos_div_2 eps))) => {H} /= n2 H.
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    set n := (n1 + n2)%nat.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move: (fun y Hy => Hfn n (le_plus_l _ _) y Hy) => {Hfn} Hfn.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move: (H n (le_plus_r _ _)) => {H} H.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move: (Hex x n Hx) => {Hex} Hex.
(* Goal: @locally' R_UniformSpace x (fun y : R => Rlt (Rabs (Rminus (real (Lim_seq (fun n : nat => fn n y))) l)) (pos eps)) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
    apply Lim_correct' in Hex.
(* Goal: @locally' R_UniformSpace x (fun y : R => Rlt (Rabs (Rminus (real (Lim_seq (fun n : nat => fn n y))) l)) (pos eps)) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
    apply is_lim_spec in Hex.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (Hex (pos_div_2 eps)) => {Hex} /= d1 Hex.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (Ho x Hx) => {Ho} /= d0 Ho.
(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
    have Hd : 0 < Rmin d0 d1.
(* Goal: Rlt (IZR Z0) (Rmin (pos d0) (pos d1)) *)
(* Goal: @locally' R_UniformSpace x (fun y : R => Rlt (Rabs (Rminus (real (Lim_seq (fun n : nat => fn n y))) l)) (pos eps)) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
      apply Rmin_case ; [by apply d0 | by apply d1].
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    exists (mkposreal _ Hd) => /= y Hy Hxy.
    replace (real (Lim_seq (fun n0 : nat => fn n0 y)) - l)
      with ((real (Lim (fn n) x) - l)
            - (fn n y - real (Lim_seq (fun n : nat => fn n y)))
            + (fn n y - real (Lim (fn n) x)))
(* Goal: @eq R (Rminus (Rplus (sum_f_R0 An n) (Series (fun k : nat => An (S (Init.Nat.add n k))))) (sum_f_R0 An n)) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule An *)
(* Goal: is_lim_seq (fun n : nat => Rminus (Series An) (sum_f_R0 An n)) (Finite (IZR Z0)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
      by ring.
    rewrite (double_var eps) ;
    apply Rle_lt_trans with (1 := Rabs_triang _ _), Rplus_lt_compat.
    rewrite (double_var (eps/2)) ;
    apply Rle_lt_trans with (1 := Rabs_triang _ _), Rplus_lt_compat.
(* Goal: Rlt (dist R_met y x) d *)
    exact: H.
(* Goal: Rlt (Rabs (Ropp (Rminus (fn n y) (real (Lim_seq (fun n : nat => fn n y)))))) (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (real (Lim (fn n) (Finite x))))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
    rewrite Rabs_Ropp ; apply Hfn.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Ho, Rlt_le_trans with (1 := Hy), Rmin_l.
(* Goal: Rlt (Rabs (Rminus (fn n y) (real (Lim (fn n) (Finite x))))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
    apply Hex.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Rlt_le_trans with (1 := Hy), Rmin_r.
(* Goal: Rlt (dist R_met y x) d *)
    exact: Hxy.
(* Goal: D_x no_cond x y *)
(* Goal: Rlt (dist R_met y x) d *)
  split.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by exists l.
(* Goal: @eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))) *)
  replace l with (real l) by auto.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply sym_eq, (f_equal real), is_lim_unique.
Qed.
Lemma CVU_cont_open (fn : nat -> R -> R) (D : R -> Prop) :
  open D ->
  CVU_dom fn D ->
  (forall n, forall x, D x -> continuity_pt (fn n) x)
    -> forall x, D x -> continuity_pt (fun y => real (Lim_seq (fun n => fn n y))) x.
Proof.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move => Ho Hfn Hc x Hx.
  case: (fun H => CVU_limits_open fn D Ho Hfn H x Hx)
    => [{x Hx} x n Hx | Hex_s [Hex_f Heq]].
(* Goal: ex_finite_lim (fn n) (Finite x) *)
(* Goal: continuity_pt (fun y : R => real (Lim_seq (fun n : nat => fn n y))) x *)
  exists (fn n x).
(* Goal: is_lim (fn n) (Finite x) (Finite (fn n x)) *)
  apply is_lim_spec.
(* Goal: is_lim' (fn n) (Finite x) (Finite (fn n x)) *)
(* Goal: continuity_pt (fun y : R => real (Lim_seq (fun n : nat => fn n y))) x *)
  intros eps.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (Hc n x Hx eps (cond_pos eps)) => {Hc} d [Hd Hc].
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  exists (mkposreal d Hd) => /= y Hy Hxy.
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn n x))) (pos eps) *)
  apply (Hc y).
(* Goal: D_x no_cond x y *)
(* Goal: Rlt (dist R_met y x) d *)
  split.
(* Goal: D_x no_cond x y *)
(* Goal: Rlt (dist R_met y x) d *)
  split.
(* Goal: Rlt (dist R_met y x) d *)
  exact: I.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply sym_not_eq, Hxy.
(* Goal: Rlt (dist R_met y x) d *)
  exact: Hy.
(* Goal: continuity_pt (fun y : R => real (Lim_seq (fun n : nat => fn n y))) x *)
  apply Lim_correct' in Hex_f.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  rewrite -Heq in Hex_f => {Heq}.
  replace (Lim_seq (fun n : nat => real (Lim (fn n) x)))
    with (Lim_seq (fun n : nat => (fn n) x)) in Hex_f.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move => e He.
(* Goal: @ex R (fun alp : R => and (Rgt alp (IZR Z0)) (forall (x0 : Base R_met) (_ : and (D_x no_cond x x0) (Rlt (dist R_met x0 x) alp)), Rlt (dist R_met (real (Lim_seq (fun n : nat => fn n x0))) (real (Lim_seq (fun n : nat => fn n x)))) e)) *)
(* Goal: @eq Rbar (Lim_seq (fun n : nat => fn n x)) (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) *)
  apply is_lim_spec in Hex_f.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (Hex_f (mkposreal e He)) => {Hex_f} /= delta Hex_f.
(* Goal: @ex R (fun alp : R => and (Rgt alp (IZR Z0)) (forall (x0 : R) (_ : and (D_x no_cond x x0) (Rlt (R_dist x0 x) alp)), Rlt (R_dist (real (Lim_seq (fun n : nat => fn n x0))) (real (Lim_seq (fun n : nat => fn n x)))) e)) *)
(* Goal: @eq Rbar (Lim_seq (fun n : nat => fn n x)) (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) *)
  exists delta ; split => [ | y [[_ Hxy] Hy]].
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply delta.
(* Goal: Rlt (R_dist (real (Lim_seq (fun n : nat => fn n y))) (real (Lim_seq (fun n : nat => fn n x)))) e *)
(* Goal: @eq Rbar (Lim_seq (fun n : nat => fn n x)) (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) *)
  apply Hex_f.
(* Goal: Rlt (dist R_met y x) d *)
  exact: Hy.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply sym_not_eq.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  apply Lim_seq_ext => n.
(* Goal: @eq R (fn n x) (real (Lim (fn n) (Finite x))) *)
  replace (fn n x) with (real (fn n x)) by auto.
(* Goal: @eq R (real (Finite (fn n x))) (real (Lim (fn n) (Finite x))) *)
  apply sym_eq, f_equal, is_lim_unique.
(* Goal: is_lim (fn n) (Finite x) (Finite (fn n x)) *)
  apply is_lim_spec.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move => eps.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (Hc n x Hx eps (cond_pos eps)) => {Hc} d [Hd Hc].
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  exists (mkposreal d Hd) => /= y Hy Hxy.
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn n x))) (pos eps) *)
  apply (Hc y).
(* Goal: D_x no_cond x y *)
(* Goal: Rlt (dist R_met y x) d *)
  split.
(* Goal: D_x no_cond x y *)
(* Goal: Rlt (dist R_met y x) d *)
  split.
(* Goal: Rlt (dist R_met y x) d *)
  exact: I.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply sym_not_eq, Hxy.
(* Goal: Rlt (dist R_met y x) d *)
  exact: Hy.
Qed.

Lemma CVU_Derive (fn : nat -> R -> R) (D : R -> Prop) :
  open D -> is_connected D
  -> CVU_dom fn D
  -> (forall n x, D x -> ex_derive (fn n) x)
  -> (forall n x, D x -> continuity_pt (Derive (fn n)) x)
  -> CVU_dom (fun n x => Derive (fn n) x) D
  -> (forall x , D x ->
       (is_derive (fun y => real (Lim_seq (fun n => fn n y))) x
         (real (Lim_seq (fun n => Derive (fn n) x))))).
Proof.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move => Ho Hc Hfn Edn Cdn Hdn.

  set rn := fun x n h => match (Req_EM_T h 0) with
    | left _ => Derive (fn n) x
    | right _ => (fn n (x+h) - fn n x)/h
  end.

  assert (Ho' : forall x : R, open (fun h : R => D (x + h))).
    intros x.
    apply open_comp with (2 := Ho).
    intros t _.
    eapply (filterlim_comp_2 (F := locally t)).
    apply filterlim_const.
    apply filterlim_id.
    apply: filterlim_plus.

(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
  have Crn : forall x, D x -> forall n h, D (x+h) -> is_lim (rn x n) h (rn x n h).
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move => x Hx n h Hh.
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S (S (@seq.size R a_)))) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R a0 (@Datatypes.cons R a1 a_)) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.cons R a1 a_) i)))) *)
(* Goal: forall _ : @ex nat (fun i : nat => and (lt (S i) (@seq.size R a_)) (and (Rle (@seq.nth R (IZR Z0) a_ i) x) (Rle x (@seq.nth R (IZR Z0) a_ (S i))))), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps)) *)
    rewrite {2}/rn ; case: (Req_EM_T h 0) => [-> | Hh0].
(* Goal: is_lim (fn n) (Finite x) (Finite (fn n x)) *)
    apply is_lim_spec.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move => eps.
    cut (locally 0 (fun y : R => y <> 0 ->
      Rabs ((fn n (x + y) - fn n x) / y - Derive (fn n) x) < eps)).
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case => d H.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    exists d => y Hy Hxy.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    rewrite /rn ; case: Req_EM_T => // _ ; by apply H.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move: (Edn n x Hx) => {Edn} Edn.
    apply Derive_correct in Edn.
    apply is_derive_Reals in Edn.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (Edn eps (cond_pos eps)) => {Edn} delta Edn.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    exists delta => y Hy Hxy.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /= in Hy.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite -/(Rminus _ _) Rminus_0_r in Hy.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Edn.

(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
    have H : continuity_pt (fun h => ((fn n (x + h) - fn n x) / h)) h.
      apply derivable_continuous_pt.
      apply derivable_pt_div.
      apply derivable_pt_minus.
      apply derivable_pt_comp.
      apply (derivable_pt_plus (fun _ => x) (fun h => h) h).
(* Goal: Rlt (dist R_met y x) d *)
      exact: derivable_pt_const.
(* Goal: Rlt (dist R_met y x) d *)
      exact: derivable_pt_id.
      exists (Derive (fn n) (x + h)) ; by apply is_derive_Reals, Derive_correct, Edn.
(* Goal: Rlt (dist R_met y x) d *)
      exact: derivable_pt_const.
(* Goal: Rlt (dist R_met y x) d *)
      exact: derivable_pt_id.
(* Goal: Rlt (dist R_met y x) d *)
      exact: Hh0.

(* Goal: is_lim (fn n) (Finite x) (Finite (fn n x)) *)
    apply is_lim_spec.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move => eps.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (H eps (cond_pos eps)) => {H} d [Hd H].
(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
    have Hd0 : 0 < Rmin d (Rabs h).
      apply Rmin_case.
(* Goal: Rlt (dist R_met y x) d *)
      exact: Hd.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
      by apply Rabs_pos_lt.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    exists (mkposreal _ Hd0) => /= y Hy Hhy.
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S (S (@seq.size R a_)))) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R a0 (@Datatypes.cons R a1 a_)) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.cons R a1 a_) i)))) *)
(* Goal: forall _ : @ex nat (fun i : nat => and (lt (S i) (@seq.size R a_)) (and (Rle (@seq.nth R (IZR Z0) a_ i) x) (Rle x (@seq.nth R (IZR Z0) a_ (S i))))), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps)) *)
    rewrite /rn ; case: Req_EM_T => /= Hy'.
    contradict Hy.
    apply Rle_not_lt.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite /abs /minus /plus /opp /=.
(* Goal: Rlt (IZR Z0) (Rminus y x) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn m y))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
    rewrite Hy' -/(Rminus _ _) Rminus_0_l Rabs_Ropp ; by apply Rmin_r.
(* Goal: D_x no_cond x y *)
(* Goal: Rlt (dist R_met y x) d *)
    apply (H y) ; split.
(* Goal: D_x no_cond x y *)
(* Goal: Rlt (dist R_met y x) d *)
    split.
(* Goal: Rlt (dist R_met y x) d *)
    exact: I.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply sym_not_eq.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Rlt_le_trans with (1 := Hy), Rmin_l.


(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
  have Hrn : forall x, D x -> CVU_dom (rn x) (fun h : R => D (x + h)).
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move => x Hx.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    apply CVU_dom_cauchy => eps.
    apply CVU_dom_cauchy in Hdn.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (Hdn eps) => {Hdn} /= N Hdn.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    exists N => n m h Hh Hn Hm.
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S (S (@seq.size R a_)))) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R a0 (@Datatypes.cons R a1 a_)) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.cons R a1 a_) i)))) *)
(* Goal: forall _ : @ex nat (fun i : nat => and (lt (S i) (@seq.size R a_)) (and (Rle (@seq.nth R (IZR Z0) a_ i) x) (Rle x (@seq.nth R (IZR Z0) a_ (S i))))), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps)) *)
    rewrite /rn ; case: Req_EM_T => Hh0.
(* Goal: Rlt (dist R_met y x) d *)
    exact: (Hdn n m x Hx Hn Hm).
    replace ((fn n (x + h) - fn n x) / h - (fn m (x + h) - fn m x) / h)
      with (((fn n (x + h) - fn m (x + h)) - (fn n x - fn m x))/h)
      by (field ; auto).
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (MVT_gen (fun x => (fn n x - fn m x)) x (x+h) (Derive (fun x => fn n x - fn m x))) => [y Hy | y Hy | z [Hz ->]].
    apply Derive_correct.
    apply: ex_derive_minus ; apply Edn, (Hc (Rmin x (x + h)) (Rmax x (x + h))).
(* Goal: Rlt (IZR Z0) (Rmin (pos d0) (pos d1)) *)
(* Goal: @locally' R_UniformSpace x (fun y : R => Rlt (Rabs (Rminus (real (Lim_seq (fun n : nat => fn n y))) l)) (pos eps)) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
    apply Rmin_case ; [by apply Hx | by apply Hh].
    apply Rmax_case ; [by apply Hx | by apply Hh].
    split ; apply Rlt_le ; by apply Hy.
(* Goal: Rlt (IZR Z0) (Rmin (pos d0) (pos d1)) *)
(* Goal: @locally' R_UniformSpace x (fun y : R => Rlt (Rabs (Rminus (real (Lim_seq (fun n : nat => fn n y))) l)) (pos eps)) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
    apply Rmin_case ; [by apply Hx | by apply Hh].
    apply Rmax_case ; [by apply Hx | by apply Hh].
    split ; apply Rlt_le ; by apply Hy.
    apply derivable_continuous_pt, derivable_pt_minus.
    exists (Derive (fn n) y) ; apply is_derive_Reals, Derive_correct, Edn, (Hc (Rmin x (x + h)) (Rmax x (x + h))).
(* Goal: Rlt (IZR Z0) (Rmin (pos d0) (pos d1)) *)
(* Goal: @locally' R_UniformSpace x (fun y : R => Rlt (Rabs (Rminus (real (Lim_seq (fun n : nat => fn n y))) l)) (pos eps)) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
    apply Rmin_case ; [by apply Hx | by apply Hh].
    apply Rmax_case ; [by apply Hx | by apply Hh].
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Hy.
    exists (Derive (fn m) y) ; apply is_derive_Reals, Derive_correct, Edn, (Hc (Rmin x (x + h)) (Rmax x (x + h))).
(* Goal: Rlt (IZR Z0) (Rmin (pos d0) (pos d1)) *)
(* Goal: @locally' R_UniformSpace x (fun y : R => Rlt (Rabs (Rminus (real (Lim_seq (fun n : nat => fn n y))) l)) (pos eps)) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
    apply Rmin_case ; [by apply Hx | by apply Hh].
    apply Rmax_case ; [by apply Hx | by apply Hh].
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Hy.
    replace (Derive (fun x1 : R => fn n x1 - fn m x1) z * (x + h - x) / h)
      with (Derive (fun x1 : R => fn n x1 - fn m x1) z)
      by (field ; auto).
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite Derive_minus.
    apply (Hdn n m z).
    apply (Hc (Rmin x (x + h)) (Rmax x (x + h))).
(* Goal: Rlt (IZR Z0) (Rmin (pos d0) (pos d1)) *)
(* Goal: @locally' R_UniformSpace x (fun y : R => Rlt (Rabs (Rminus (real (Lim_seq (fun n : nat => fn n y))) l)) (pos eps)) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
    apply Rmin_case ; [by apply Hx | by apply Hh].
    apply Rmax_case ; [by apply Hx | by apply Hh].
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Hz.
(* Goal: Rlt (dist R_met y x) d *)
    exact: Hn.
(* Goal: Rlt (dist R_met y x) d *)
    exact: Hm.
    apply Edn, (Hc (Rmin x (x + h)) (Rmax x (x + h))).
(* Goal: Rlt (IZR Z0) (Rmin (pos d0) (pos d1)) *)
(* Goal: @locally' R_UniformSpace x (fun y : R => Rlt (Rabs (Rminus (real (Lim_seq (fun n : nat => fn n y))) l)) (pos eps)) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
    apply Rmin_case ; [by apply Hx | by apply Hh].
    apply Rmax_case ; [by apply Hx | by apply Hh].
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Hz.
    apply Edn, (Hc (Rmin x (x + h)) (Rmax x (x + h))).
(* Goal: Rlt (IZR Z0) (Rmin (pos d0) (pos d1)) *)
(* Goal: @locally' R_UniformSpace x (fun y : R => Rlt (Rabs (Rminus (real (Lim_seq (fun n : nat => fn n y))) l)) (pos eps)) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
    apply Rmin_case ; [by apply Hx | by apply Hh].
    apply Rmax_case ; [by apply Hx | by apply Hh].
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Hz.

  have Lrn : forall x, D x -> (forall (y : R) (n : nat),
    (fun h : R => D (x + h)) y -> ex_finite_lim (rn x n) y).
    intros ; exists (rn x n y) ; by intuition.

(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move => x Hx.

(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (CVU_limits_open (rn x) _ (Ho' x) (Hrn x Hx) (Lrn x Hx) 0) => [ | H [H0 H1]].
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by rewrite Rplus_0_r.

  have : ex_derive (fun y : R => real (Lim_seq (fun n : nat => fn n y))) x
    /\ Derive (fun y : R => real (Lim_seq (fun n : nat => fn n y))) x
      = real (Lim_seq (fun n : nat => Derive (fn n) x)).

(* Goal: D_x no_cond x y *)
(* Goal: Rlt (dist R_met y x) d *)
  split.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: H0 => df H0.
  exists df.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  apply is_derive_Reals => e He.
  apply is_lim_spec in H0.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (H0 (mkposreal e He)) => {H0} /= delta H0.
  destruct (Ho x Hx) as [dx Hd].
(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
  have H2 : 0 < Rmin delta dx.
(* Goal: Rlt (IZR Z0) (Rmin (pos d0) (pos d1)) *)
(* Goal: @locally' R_UniformSpace x (fun y : R => Rlt (Rabs (Rminus (real (Lim_seq (fun n : nat => fn n y))) l)) (pos eps)) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
    apply Rmin_case ; [by apply delta | by apply dx].
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  exists (mkposreal _ H2) => /= h Hh0 Hh.
  replace (real (Lim_seq (fun n : nat => fn n (x + h))) -
    real (Lim_seq (fun n : nat => fn n x))) with
    (real (Rbar_minus (Lim_seq (fun n : nat => fn n (x + h))) (Lim_seq (fun n : nat => fn n x)))).
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite -Lim_seq_minus.
  replace (real (Lim_seq (fun n : nat => fn n (x + h) - fn n x)) / h)
  with (real (Rbar_mult (/h) (Lim_seq (fun n : nat => fn n (x + h) - fn n x)))).
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite -Lim_seq_scal_l.
  replace (Lim_seq (fun n : nat => / h * (fn n (x + h) - fn n x)))
    with (Lim_seq (fun n : nat => rn x n h)).
  apply H0.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /=.
  rewrite -/(Rminus _ _) Rminus_0_r ; apply Rlt_le_trans with (1 := Hh), Rmin_l.
(* Goal: Rlt (dist R_met y x) d *)
  exact: Hh0.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  apply Lim_seq_ext => n.
  rewrite /rn /Rdiv ; case: Req_EM_T => // _ ; exact: Rmult_comm.
  case: (Lim_seq (fun n : nat => fn n (x + h) - fn n x))
    => [l | | ] //=.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by field.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite /Rdiv Rmult_0_l.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: Rle_dec => // Hh1.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: Rle_lt_or_eq_dec => //.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite /Rdiv Rmult_0_l.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: Rle_dec => // Hh1.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: Rle_lt_or_eq_dec => //.

  apply ex_finite_lim_seq_correct, CVU_CVS_dom with D.
(* Goal: Rlt (dist R_met y x) d *)
  exact: Hfn.
  apply Hd.
(* Goal: Rlt (Rabs (Rminus (fn n y) (real (Finite (f y))))) e *)
(* Goal: CVU fn f x r *)
  simpl.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /=.
  ring_simplify (x + h + - x) ; apply Rlt_le_trans with (1 := Hh), Rmin_r.
  apply ex_finite_lim_seq_correct, CVU_CVS_dom with D.
(* Goal: Rlt (dist R_met y x) d *)
  exact: Hfn.
  apply Hd.
  apply ball_center.
  apply (CVU_CVS_dom fn D) in Hfn ; rewrite /CVS_dom in Hfn.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move: (fun H => Lim_seq_correct' _ (Hfn (x+h) (Hd _ H))) => F.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move: (fun H => Lim_seq_correct' _ (Hfn (x) (Hd _ H))) => F0.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite (is_lim_seq_unique _ (real (Lim_seq (fun n : nat => fn n (x + h))))).
  rewrite (is_lim_seq_unique  (fun n : nat => fn n (x)) (real (Lim_seq (fun n : nat => fn n (x))))).
(* Goal: is_Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An))) (Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An)))) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  easy.
  apply F0.
  apply ball_center.
  apply F.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /=.
  ring_simplify (x + h + - x).
  apply Rlt_le_trans with (1 := Hh), Rmin_r.
  apply (CVU_CVS_dom fn D) in Hfn ; rewrite /CVS_dom in Hfn.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move: (fun H => Lim_seq_correct' _ (Hfn (x+h) (Hd _ H))) => F.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move: (fun H => Lim_seq_correct' _ (Hfn (x) (Hd _ H))) => F0.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite (is_lim_seq_unique _ (real (Lim_seq (fun n : nat => fn n (x + h))))).
  rewrite (is_lim_seq_unique  (fun n : nat => fn n (x)) (real (Lim_seq (fun n : nat => fn n (x))))).
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by [].
  apply F0.
  apply ball_center.
  apply F.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /=.
  ring_simplify (x + h + - x).
  apply Rlt_le_trans with (1 := Hh), Rmin_r.

(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite /Derive.
  replace (Lim_seq (fun n : nat => real (Lim (fun h : R => (fn n (x + h) - fn n x) / h) 0)))
    with (Lim_seq (fun n : nat => real (Lim (rn x n) 0))).
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite H1.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: H0 => drn H0.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite (is_lim_unique _ _ _ H0).
  apply f_equal, is_lim_unique.
(* Goal: is_lim (fn n) (Finite x) (Finite (fn n x)) *)
  apply is_lim_spec.
(* Goal: is_lim' (fn n) (Finite x) (Finite (fn n x)) *)
(* Goal: continuity_pt (fun y : R => real (Lim_seq (fun n : nat => fn n y))) x *)
  intros eps.
  apply is_lim_spec in H0.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (H0 eps) => {H0} delta H0.
  destruct (Ho x Hx) as [dx Hd].
(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
  have H2 : 0 < Rmin delta dx.
(* Goal: Rlt (IZR Z0) (Rmin (pos d0) (pos d1)) *)
(* Goal: @locally' R_UniformSpace x (fun y : R => Rlt (Rabs (Rminus (real (Lim_seq (fun n : nat => fn n y))) l)) (pos eps)) *)
(* Goal: and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R l (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)))) *)
    apply Rmin_case ; [by apply delta | by apply dx].
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  exists (mkposreal _ H2) => /= h Hh0 Hh.
  replace (real (Lim_seq (fun n : nat => fn n (x + h))) -
    real (Lim_seq (fun n : nat => fn n x))) with
    (real (Rbar_minus (Lim_seq (fun n : nat => fn n (x + h))) (Lim_seq (fun n : nat => fn n x)))).
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite -Lim_seq_minus.
  replace (real (Lim_seq (fun n : nat => fn n (x + h) - fn n x)) / h)
  with (real (Rbar_mult (/h) (Lim_seq (fun n : nat => fn n (x + h) - fn n x)))).
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite -Lim_seq_scal_l.
  replace (Lim_seq (fun n : nat => / h * (fn n (x + h) - fn n x)))
    with (Lim_seq (fun n : nat => rn x n h)).
  apply H0.
  apply Rlt_le_trans with (1 := Hh0), Rmin_l.
(* Goal: Rlt (dist R_met y x) d *)
  exact: Hh.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  apply Lim_seq_ext => n.
  rewrite /rn /Rdiv ; case: Req_EM_T => // _ ; exact: Rmult_comm.
  case: (Lim_seq (fun n : nat => fn n (x + h) - fn n x))
    => [l | | ] //=.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by field.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite /Rdiv Rmult_0_l.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: Rle_dec => // Hh1.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: Rle_lt_or_eq_dec => //.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite /Rdiv Rmult_0_l.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: Rle_dec => // Hh1.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: Rle_lt_or_eq_dec => //.

  apply ex_finite_lim_seq_correct, CVU_CVS_dom with D.
(* Goal: Rlt (dist R_met y x) d *)
  exact: Hfn.
  apply Hd.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /=.
  ring_simplify (x + h + - x) ; rewrite -(Rminus_0_r h) ;
  apply Rlt_le_trans with (1 := Hh0), Rmin_r.
  apply ex_finite_lim_seq_correct, CVU_CVS_dom with D.
(* Goal: Rlt (dist R_met y x) d *)
  exact: Hfn.
  apply Hd.
  apply ball_center.
  apply (CVU_CVS_dom fn D) in Hfn ; rewrite /CVS_dom in Hfn.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move: (fun H => Lim_seq_correct' _ (Hfn (x+h) (Hd _ H))) => F.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move: (fun H => Lim_seq_correct' _ (Hfn (x) (Hd _ H))) => F0.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite (is_lim_seq_unique _ (real (Lim_seq (fun n : nat => fn n (x + h))))).
  rewrite (is_lim_seq_unique  (fun n : nat => fn n (x)) (real (Lim_seq (fun n : nat => fn n (x))))).
(* Goal: is_Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An))) (Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An)))) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  easy.
  apply F0.
  apply ball_center.
  apply F.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /=.
  ring_simplify (x + h + - x).
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /= in Hh0.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite -/(Rminus _ _) Rminus_0_r in Hh0.
  apply Rlt_le_trans with (1 := Hh0), Rmin_r.
  apply (CVU_CVS_dom fn D) in Hfn ; rewrite /CVS_dom in Hfn.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move: (fun H => Lim_seq_correct' _ (Hfn (x+h) (Hd _ H))) => F.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move: (fun H => Lim_seq_correct' _ (Hfn (x) (Hd _ H))) => F0.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite (is_lim_seq_unique _ (real (Lim_seq (fun n : nat => fn n (x + h))))).
  rewrite (is_lim_seq_unique  (fun n : nat => fn n (x)) (real (Lim_seq (fun n : nat => fn n (x))))).
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by [].
  apply F0.
  apply ball_center.
  apply F.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /=.
  ring_simplify (x + h + - x).
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /= in Hh0.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite -/(Rminus _ _) Rminus_0_r in Hh0.
  apply Rlt_le_trans with (1 := Hh0), Rmin_r.

(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  apply Lim_seq_ext => n.
(* Goal: @eq R (real (Finite (fn n x))) (real (Lim (fn n) (Finite x))) *)
  apply sym_eq, f_equal, is_lim_unique.
(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
  have Hx' : D (x + 0).
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by rewrite Rplus_0_r.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite (is_lim_unique _ _ _ (Crn x Hx n 0 Hx')).
(* Goal: is_lim (fn n) (Finite x) (Finite (fn n x)) *)
  apply is_lim_spec.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move: (Crn x Hx n 0 Hx') => H2 eps.
  apply is_lim_spec in H2.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (H2 eps) => {H2} delta H2.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  exists delta => y Hy Hy0.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move: (H2 y Hy Hy0).
(* Goal: Rlt (IZR Z0) (Rminus y x) *)
(* Goal: Rlt (Rabs (Rminus (fn n y) (fn m y))) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: and (ex_finite_lim_seq (fun n : nat => real (Lim (fn n) (Finite x)))) (and (ex_finite_lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x)) (@eq R (real (Lim_seq (fun n : nat => real (Lim (fn n) (Finite x))))) (real (Lim (fun y : R => real (Lim_seq (fun n : nat => fn n y))) (Finite x))))) *)
  rewrite {1}/rn ; by case: Req_EM_T.

(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case => H2 H3.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite -H3.
  by apply Derive_correct.
Qed.

(** ** Dini's theorem *)

Lemma Dini (fn : nat -> R -> R) (a b : R) :
  a < b -> CVS_dom fn (fun x => a <= x <= b)
  -> (forall (n : nat) (x : R), a <= x <= b -> continuity_pt (fn n) x)
  -> (forall (x : R), a <= x <= b -> continuity_pt (fun y => Lim_seq (fun n => fn n y)) x)
  -> (forall (n : nat) (x y : R), a <= x -> x <= y -> y <= b -> fn n x <= fn n y)
  -> CVU_dom fn (fun x => a <= x <= b).
Proof.
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  set AB := fun x => a <= x <= b.
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  set f : R -> R := (fun y : R => Lim_seq (fun n : nat => fn n y)).
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move => Hab Hcvs Cfn Cf Hfn.

(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
  have CUf : uniform_continuity f AB.
(* Goal: uniform_continuity f AB *)
(* Goal: CVU_dom fn AB *)
    apply Heine.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply compact_P3.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Cf.
  suff H : forall eps : posreal, exists N : nat,
    forall n : nat, (N <= n)%nat -> forall x : R, AB x ->
    Rabs (fn n x - Lim_seq (fun n0 : nat => fn n0 x)) < 5 * eps.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move => eps.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    replace (pos eps) with (5 * (eps / 5)) by field.
(* Goal: eventually (fun n : nat => forall (x : R) (_ : AB x), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (Rdiv (pos eps) (IZR (Zpos (xI (xO xH))))))) *)
(* Goal: forall eps : posreal, @ex nat (fun N : nat => forall (n : nat) (_ : le N n) (x : R) (_ : AB x), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps))) *)
    suff He : 0 < eps / 5.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply (H (mkposreal _ He)).
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (IZR (Zpos (xI (xO xH))))) *)
(* Goal: forall eps : posreal, @ex nat (fun N : nat => forall (n : nat) (_ : le N n) (x : R) (_ : AB x), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps))) *)
    apply Rdiv_lt_0_compat.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply eps.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xI (xO xH)))) *)
(* Goal: forall eps : posreal, @ex nat (fun N : nat => forall (n : nat) (_ : le N n) (x : R) (_ : AB x), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps))) *)
    repeat (apply Rplus_lt_0_compat || apply Rmult_lt_0_compat) ; apply Rlt_0_1.

(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move => eps.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (CUf eps) => {CUf} eta CUf.
  move: (interval_finite_subdiv_between  a b (pos_div_2 eta) (Rlt_le _ _ Hab)).
  case: (interval_finite_subdiv a b (pos_div_2 eta) (Rlt_le _ _ Hab)) =>
    a_ Ha_ /= Ha_0.
  have : exists N, forall n i, (N <= n)%nat -> (i < seq.size a_)%nat
    -> Rabs (fn n (seq.nth 0 a_ i) - f (seq.nth 0 a_ i)) < eps.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: a_ Ha_ Ha_0 => [ | a0 a_] Ha_ /= Ha_0.
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S O)) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R a0 (@Datatypes.nil R)) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.nil R) i)))) *)
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S (S (@seq.size R a_)))) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R a0 (@Datatypes.cons R a1 a_)) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.cons R a1 a_) i)))) *)
(* Goal: forall _ : @ex nat (fun i : nat => and (lt (S i) (@seq.size R a_)) (and (Rle (@seq.nth R (IZR Z0) a_ i) x) (Rle x (@seq.nth R (IZR Z0) a_ (S i))))), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps)) *)
    contradict Hab.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite -(proj1 Ha_) -(proj1 (proj2 Ha_)).
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Rlt_irrefl.
(* Goal: forall n : nat, @eq R (@sum_n R_AbelianGroup (fun k : nat => An k) n) (sum_f_R0 An n) *)
(* Goal: is_lim_seq (@sum_n R_AbelianGroup (fun k : nat => An k)) (Finite (real (Lim_seq (@sum_n R_AbelianGroup An)))) *)
(* Goal: is_Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An))) (Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An)))) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    elim: (a_) (a0) Ha_0 => /= [ | x1 l IH] x0 Hl.
    move: (Hcvs x0 (Hl O (lt_n_Sn _))) ;
    move/Lim_seq_correct' => {Hcvs} Hcvs.
(* Goal: @ex nat (fun N : nat => forall (n i : nat) (_ : le N n) (_ : lt i (S (S (@seq.size R l)))), Rlt (Rabs (Rminus (fn n (@seq.nth R (IZR Z0) (@Datatypes.cons R x0 (@Datatypes.cons R x1 l)) i)) (f (@seq.nth R (IZR Z0) (@Datatypes.cons R x0 (@Datatypes.cons R x1 l)) i)))) (pos eps)) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n i : nat) (_ : le N n) (_ : lt i (@seq.size R a_)), Rlt (Rabs (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i)))) (pos eps)), @ex nat (fun N : nat => forall (n : nat) (_ : le N n) (x0 : R) (_ : AB x0), Rlt (Rabs (Rminus (fn n x0) (real (Lim_seq (fun n0 : nat => fn n0 x0))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps))) *)
    apply is_lim_seq_spec in Hcvs.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (Hcvs eps) => {Hcvs} N Hcvs.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    exists N => n i Hn Hi.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: i Hi => /= [ | i] Hi.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Hcvs.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply lt_S_n, lt_n_O in Hi.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (IH x1).
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move => i Hi.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply (Hl (S i)), lt_n_S.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move => N0 HN0.
    move: (Hcvs x0 (Hl O (lt_O_Sn _))) ;
    move/Lim_seq_correct' => {Hcvs} Hcvs.
(* Goal: @ex nat (fun N : nat => forall (n i : nat) (_ : le N n) (_ : lt i (S (S (@seq.size R l)))), Rlt (Rabs (Rminus (fn n (@seq.nth R (IZR Z0) (@Datatypes.cons R x0 (@Datatypes.cons R x1 l)) i)) (f (@seq.nth R (IZR Z0) (@Datatypes.cons R x0 (@Datatypes.cons R x1 l)) i)))) (pos eps)) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n i : nat) (_ : le N n) (_ : lt i (@seq.size R a_)), Rlt (Rabs (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i)))) (pos eps)), @ex nat (fun N : nat => forall (n : nat) (_ : le N n) (x0 : R) (_ : AB x0), Rlt (Rabs (Rminus (fn n x0) (real (Lim_seq (fun n0 : nat => fn n0 x0))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps))) *)
    apply is_lim_seq_spec in Hcvs.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (Hcvs eps) => {Hcvs} N Hcvs.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    exists (N + N0)%nat => n i Hn Hi.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: i Hi => /= [ | i ] Hi.
(* Goal: Rlt (Rabs (Rminus (fn n x0) (f x0))) (pos eps) *)
(* Goal: Rlt (Rabs (Rminus (fn n (@seq.nth R (IZR Z0) (@Datatypes.cons R x1 l) i)) (f (@seq.nth R (IZR Z0) (@Datatypes.cons R x1 l) i)))) (pos eps) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n i : nat) (_ : le N n) (_ : lt i (@seq.size R a_)), Rlt (Rabs (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i)))) (pos eps)), @ex nat (fun N : nat => forall (n : nat) (_ : le N n) (x0 : R) (_ : AB x0), Rlt (Rabs (Rminus (fn n x0) (real (Lim_seq (fun n0 : nat => fn n0 x0))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps))) *)
    apply Hcvs ; by intuition.
(* Goal: Rlt (Rabs (Rminus (fn n (@seq.nth R (IZR Z0) (@Datatypes.cons R x1 l) i)) (f (@seq.nth R (IZR Z0) (@Datatypes.cons R x1 l) i)))) (pos eps) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n i : nat) (_ : le N n) (_ : lt i (@seq.size R a_)), Rlt (Rabs (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i)))) (pos eps)), @ex nat (fun N : nat => forall (n : nat) (_ : le N n) (x0 : R) (_ : AB x0), Rlt (Rabs (Rminus (fn n x0) (real (Lim_seq (fun n0 : nat => fn n0 x0))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps))) *)
    apply HN0 ; by intuition.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case => N HN.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  exists N => n Hn x Hx.
(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
  have : exists i, (S i < seq.size a_)%nat /\ seq.nth 0 a_ i <= x <= seq.nth 0 a_ (S i).
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: a_ Ha_ Ha_0 {HN} => [ | a0 a_] Ha_ /= Ha_0.
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S O)) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R a0 (@Datatypes.nil R)) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.nil R) i)))) *)
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S (S (@seq.size R a_)))) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R a0 (@Datatypes.cons R a1 a_)) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.cons R a1 a_) i)))) *)
(* Goal: forall _ : @ex nat (fun i : nat => and (lt (S i) (@seq.size R a_)) (and (Rle (@seq.nth R (IZR Z0) a_ i) x) (Rle x (@seq.nth R (IZR Z0) a_ (S i))))), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps)) *)
    contradict Hab.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite -(proj1 Ha_) -(proj1 (proj2 Ha_)).
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Rlt_irrefl.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: a_ Ha_ Ha_0 => [ | a1 a_] Ha_ /= Ha_0.
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S O)) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R a0 (@Datatypes.nil R)) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.nil R) i)))) *)
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S (S (@seq.size R a_)))) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R a0 (@Datatypes.cons R a1 a_)) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.cons R a1 a_) i)))) *)
(* Goal: forall _ : @ex nat (fun i : nat => and (lt (S i) (@seq.size R a_)) (and (Rle (@seq.nth R (IZR Z0) a_ i) x) (Rle x (@seq.nth R (IZR Z0) a_ (S i))))), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps)) *)
    contradict Hab.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite -(proj1 Ha_) -(proj1 (proj2 Ha_)).
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Rlt_irrefl.
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S (S (@seq.size R a_)))) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R a0 (@Datatypes.cons R a1 a_)) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.cons R a1 a_) i)))) *)
(* Goal: forall _ : @ex nat (fun i : nat => and (lt (S i) (@seq.size R a_)) (and (Rle (@seq.nth R (IZR Z0) a_ i) x) (Rle x (@seq.nth R (IZR Z0) a_ (S i))))), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps)) *)
    rewrite -(proj1 Ha_) in AB Hcvs CUf Hx Hab Cfn Cf Hfn Ha_0 |- * ; case: Ha_ => {a} _ Ha_.
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S (S (@seq.size R a_)))) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R a0 (@Datatypes.cons R a1 a_)) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.cons R a1 a_) i)))) *)
(* Goal: forall _ : @ex nat (fun i : nat => and (lt (S i) (@seq.size R a_)) (and (Rle (@seq.nth R (IZR Z0) a_ i) x) (Rle x (@seq.nth R (IZR Z0) a_ (S i))))), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps)) *)
    rewrite -(proj1 Ha_) in AB Hcvs CUf Hx Hab Cfn Cf Hfn Ha_0 |- * ; case: Ha_ => {b} _ Ha_.
    clear Hcvs CUf ;
    revert AB Hx ;
    elim: (a_) (a0) (a1) => /= [ | x2 l IH] x0 x1 Hx.
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S (S (S (@seq.size R l))))) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R x0 (@Datatypes.cons R x1 (@Datatypes.cons R x2 l))) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.cons R x1 (@Datatypes.cons R x2 l)) i)))) *)
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S (S (S (@seq.size R l))))) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R x0 (@Datatypes.cons R x1 (@Datatypes.cons R x2 l))) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.cons R x1 (@Datatypes.cons R x2 l)) i)))) *)
(* Goal: forall _ : @ex nat (fun i : nat => and (lt (S i) (@seq.size R a_)) (and (Rle (@seq.nth R (IZR Z0) a_ i) x) (Rle x (@seq.nth R (IZR Z0) a_ (S i))))), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps)) *)
    exists O ; split => /=.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply lt_n_Sn.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Hx.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (Rlt_le_dec x x1) => Hx'.
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S (S (S (@seq.size R l))))) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R x0 (@Datatypes.cons R x1 (@Datatypes.cons R x2 l))) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.cons R x1 (@Datatypes.cons R x2 l)) i)))) *)
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S (S (S (@seq.size R l))))) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R x0 (@Datatypes.cons R x1 (@Datatypes.cons R x2 l))) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.cons R x1 (@Datatypes.cons R x2 l)) i)))) *)
(* Goal: forall _ : @ex nat (fun i : nat => and (lt (S i) (@seq.size R a_)) (and (Rle (@seq.nth R (IZR Z0) a_ i) x) (Rle x (@seq.nth R (IZR Z0) a_ (S i))))), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps)) *)
    exists O ; split => /=.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply lt_n_S, lt_O_Sn.
(* Goal: and (Rle x0 x) (Rle x x1) *)
(* Goal: @ex nat (fun i : nat => and (lt (S i) (S (S (S (@seq.size R l))))) (and (Rle (@seq.nth R (IZR Z0) (@Datatypes.cons R x0 (@Datatypes.cons R x1 (@Datatypes.cons R x2 l))) i) x) (Rle x (@seq.nth R (IZR Z0) (@Datatypes.cons R x1 (@Datatypes.cons R x2 l)) i)))) *)
(* Goal: forall _ : @ex nat (fun i : nat => and (lt (S i) (@seq.size R a_)) (and (Rle (@seq.nth R (IZR Z0) a_ i) x) (Rle x (@seq.nth R (IZR Z0) a_ (S i))))), Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n0 : nat => fn n0 x))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps)) *)
    split ; intuition.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (IH x1 x2).
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by intuition.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move => i [Hi Hx0].
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    exists (S i) ; by intuition.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case => i [Hi Hx'].
  replace (fn n x - Lim_seq (fun n0 : nat => fn n0 x))
    with ((f (seq.nth 0 a_ i) - f x) + (fn n x - f (seq.nth 0 a_ i)))
    by (rewrite /f ; ring).
(* Goal: Rlt (Rabs (Rplus (Rminus (f (@seq.nth R (IZR Z0) a_ i)) (f x)) (Rminus (fn n x) (f (@seq.nth R (IZR Z0) a_ i))))) (Rmult (IZR (Zpos (xI (xO xH)))) (pos eps)) *)
  replace (5 * eps) with (eps + 4 * eps) by ring.
(* Goal: Rlt (Rabs (Rminus (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ (S i)))) (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i))))) (Rplus (pos eps) (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (pos eps) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_lt_trans with (1 := Rabs_triang _ _).
(* Goal: Rlt (Rplus (Rabs (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ (S i))))) (Rabs (Ropp (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i)))))) (Rplus (pos eps) (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (pos eps) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rplus_lt_compat.
(* Goal: Rlt (Rabs (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (pos eps) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply CUf.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  apply Ha_0 ; by intuition.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply Hx.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite -Rabs_Ropp Ropp_minus_distr' Rabs_pos_eq.
(* Goal: Rlt (Rminus x (@seq.nth R (IZR Z0) a_ i)) (pos eta) *)
(* Goal: Rle (IZR Z0) (Rminus x (@seq.nth R (IZR Z0) a_ i)) *)
(* Goal: Rlt (Rabs (Rminus (fn n x) (f (@seq.nth R (IZR Z0) a_ i)))) (Rmult (IZR (Zpos (xO (xO xH)))) (pos eps)) *)
  apply Rle_lt_trans with (seq.nth 0 a_ (S i) - seq.nth 0 a_ i).
(* Goal: Rle (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
(* Goal: Rlt (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (fn n (@seq.nth R (IZR Z0) a_ i))) (Rmult (IZR (Zpos (xI xH))) (pos eps)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rplus_le_compat_r.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply Hx'.
(* Goal: Rlt (Rminus (@seq.nth R (IZR Z0) a_ (S i)) (@seq.nth R (IZR Z0) a_ i)) (pos eta) *)
(* Goal: Rle (IZR Z0) (Rminus (@seq.nth R (IZR Z0) a_ (S i)) (@seq.nth R (IZR Z0) a_ i)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_lt_trans with (eta/2).
(* Goal: Rle (Rminus (@seq.nth R (IZR Z0) a_ (S i)) (@seq.nth R (IZR Z0) a_ i)) (Rdiv (pos eta) (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (Rdiv (pos eta) (IZR (Zpos (xO xH)))) (pos eta) *)
(* Goal: Rle (IZR Z0) (Rminus (@seq.nth R (IZR Z0) a_ (S i)) (@seq.nth R (IZR Z0) a_ i)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_minus_l.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite Rplus_comm.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply Ha_.
(* Goal: Rlt (Rdiv (pos eta) (IZR (Zpos (xO xH)))) (pos eta) *)
(* Goal: Rle (IZR Z0) (Rminus (@seq.nth R (IZR Z0) a_ (S i)) (@seq.nth R (IZR Z0) a_ i)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rminus_lt_0 ; field_simplify ; rewrite Rdiv_1.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply is_pos_div_2.
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_minus_r ; rewrite Rplus_0_l.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply Hx'.
  replace (fn n x - f (seq.nth 0 a_ i))
    with ((fn n (seq.nth 0 a_ i) - f (seq.nth 0 a_ i)) + (fn n x - fn n (seq.nth 0 a_ i)))
(* Goal: @eq R (Rminus (Rplus (sum_f_R0 An n) (Series (fun k : nat => An (S (Init.Nat.add n k))))) (sum_f_R0 An n)) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule An *)
(* Goal: is_lim_seq (fun n : nat => Rminus (Series An) (sum_f_R0 An n)) (Finite (IZR Z0)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    by ring.
(* Goal: Rlt (Rabs (Rplus (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i))) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))))) (Rmult (IZR (Zpos (xO (xO xH)))) (pos eps)) *)
  replace (4 * eps) with (eps + 3 * eps) by ring.
(* Goal: Rlt (Rabs (Rminus (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ (S i)))) (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i))))) (Rplus (pos eps) (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (pos eps) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_lt_trans with (1 := Rabs_triang _ _).
(* Goal: Rlt (Rplus (Rabs (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ (S i))))) (Rabs (Ropp (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i)))))) (Rplus (pos eps) (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (pos eps) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rplus_lt_compat.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  apply HN ; by intuition.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite Rabs_pos_eq.
(* Goal: Rlt (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) (Rmult (IZR (Zpos (xI xH))) (pos eps)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_lt_trans with (fn n (seq.nth 0 a_ (S i)) - fn n (seq.nth 0 a_ i)).
(* Goal: Rle (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
(* Goal: Rlt (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (fn n (@seq.nth R (IZR Z0) a_ i))) (Rmult (IZR (Zpos (xI xH))) (pos eps)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rplus_le_compat_r.
(* Goal: Rle (fn n (@seq.nth R (IZR Z0) a_ i)) (fn n x) *)
  apply Hfn.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply Hx.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply Hx'.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply Ha_0.
  replace (fn n (seq.nth 0 a_ (S i)) - fn n (seq.nth 0 a_ i))
    with ((fn n (seq.nth 0 a_ (S i)) - f (seq.nth 0 a_ (S i)))
      - (fn n (seq.nth 0 a_ i) - f (seq.nth 0 a_ i))
      + (f (seq.nth 0 a_ (S i)) - f (seq.nth 0 a_ i)))
(* Goal: @eq R (Rminus (Rplus (sum_f_R0 An n) (Series (fun k : nat => An (S (Init.Nat.add n k))))) (sum_f_R0 An n)) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule An *)
(* Goal: is_lim_seq (fun n : nat => Rminus (Series An) (sum_f_R0 An n)) (Finite (IZR Z0)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    by ring.
(* Goal: Rlt (Rplus (Rminus (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ (S i)))) (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i)))) (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (Rmult (IZR (Zpos (xI xH))) (pos eps)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  replace (3 * eps) with ((eps + eps) + eps) by ring.
(* Goal: Rlt (Rplus (Rminus (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ (S i)))) (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i)))) (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (Rplus (Rplus (pos eps) (pos eps)) (pos eps)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_lt_trans with (1 := Rle_abs _).
(* Goal: Rlt (Rabs (Rminus (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ (S i)))) (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i))))) (Rplus (pos eps) (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (pos eps) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_lt_trans with (1 := Rabs_triang _ _).
(* Goal: Rlt (Rplus (Rabs (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ (S i))))) (Rabs (Ropp (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i)))))) (Rplus (pos eps) (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (pos eps) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rplus_lt_compat.
(* Goal: Rlt (Rabs (Rminus (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ (S i)))) (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i))))) (Rplus (pos eps) (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (pos eps) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_lt_trans with (1 := Rabs_triang _ _).
(* Goal: Rlt (Rplus (Rabs (Rminus (fn n (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ (S i))))) (Rabs (Ropp (Rminus (fn n (@seq.nth R (IZR Z0) a_ i)) (f (@seq.nth R (IZR Z0) a_ i)))))) (Rplus (pos eps) (pos eps)) *)
(* Goal: Rlt (Rabs (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (pos eps) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rplus_lt_compat.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  apply HN ; by intuition.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite Rabs_Ropp.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  apply HN ; by intuition.
(* Goal: Rlt (Rabs (Rminus (f (@seq.nth R (IZR Z0) a_ (S i))) (f (@seq.nth R (IZR Z0) a_ i)))) (pos eps) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply CUf.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  apply Ha_0 ; by intuition.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  apply Ha_0 ; by intuition.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite Rabs_pos_eq.
(* Goal: Rlt (Rminus (@seq.nth R (IZR Z0) a_ (S i)) (@seq.nth R (IZR Z0) a_ i)) (pos eta) *)
(* Goal: Rle (IZR Z0) (Rminus (@seq.nth R (IZR Z0) a_ (S i)) (@seq.nth R (IZR Z0) a_ i)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_lt_trans with (eta/2).
(* Goal: Rle (Rminus (@seq.nth R (IZR Z0) a_ (S i)) (@seq.nth R (IZR Z0) a_ i)) (Rdiv (pos eta) (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (Rdiv (pos eta) (IZR (Zpos (xO xH)))) (pos eta) *)
(* Goal: Rle (IZR Z0) (Rminus (@seq.nth R (IZR Z0) a_ (S i)) (@seq.nth R (IZR Z0) a_ i)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_minus_l.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite Rplus_comm.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply Ha_.
(* Goal: Rlt (Rdiv (pos eta) (IZR (Zpos (xO xH)))) (pos eta) *)
(* Goal: Rle (IZR Z0) (Rminus (@seq.nth R (IZR Z0) a_ (S i)) (@seq.nth R (IZR Z0) a_ i)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rminus_lt_0 ; field_simplify ; rewrite Rdiv_1.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply is_pos_div_2.
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_minus_r ; rewrite Rplus_0_l.
(* Goal: Rle (@seq.nth R (IZR Z0) a_ i) (@seq.nth R (IZR Z0) a_ (S i)) *)
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_trans with x ; apply Hx'.
(* Goal: Rle (IZR Z0) (Rminus (fn n x) (fn n (@seq.nth R (IZR Z0) a_ i))) *)
  apply Rle_minus_r ; rewrite Rplus_0_l.
(* Goal: Rle (fn n (@seq.nth R (IZR Z0) a_ i)) (fn n x) *)
  apply Hfn.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  apply Ha_0 ; by intuition.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply Hx'.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply Hx.
Qed.

(** ** Series of functions *)

Lemma CVN_CVU_r (fn : nat -> R -> R) (r : posreal) :
  CVN_r fn r -> forall x, (Rabs x < r) -> exists e : posreal,
    CVU (fun n => SP fn n) (fun x => Series (fun n => fn n x)) x e.
Proof.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case => An [l [H H0]] x Hx.
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  assert (H1 : ex_series An).
(* Goal: @ex_series R_AbsRing R_NormedModule An *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    apply ex_series_Reals_1.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    exists l => e He.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    case: (H e He) => {H} N H.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
    exists N => n Hn.
(* Goal: Rlt (R_dist (sum_f_R0 An n) l) e *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    replace (sum_f_R0 An n) with (sum_f_R0 (fun k : nat => Rabs (An k)) n).
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply H.
(* Goal: forall n : nat, @eq R (@sum_n R_AbelianGroup (fun k : nat => An k) n) (sum_f_R0 An n) *)
(* Goal: is_lim_seq (@sum_n R_AbelianGroup (fun k : nat => An k)) (Finite (real (Lim_seq (@sum_n R_AbelianGroup An)))) *)
(* Goal: is_Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An))) (Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An)))) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    elim: n {Hn} => /= [ | n IH].
(* Goal: @eq R (Rabs (An O)) (An O) *)
(* Goal: @eq R (Rplus (sum_f_R0 (fun k : nat => Rabs (An k)) n) (Rabs (An (S n)))) (Rplus (sum_f_R0 An n) (An (S n))) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    apply Rabs_pos_eq.
(* Goal: Rle (IZR Z0) (An O) *)
(* Goal: @eq R (Rplus (sum_f_R0 (fun k : nat => Rabs (An k)) n) (Rabs (An (S n)))) (Rplus (sum_f_R0 An n) (An (S n))) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    apply Rle_trans with (Rabs (fn O 0)).
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Rabs_pos.
(* Goal: Rle (Rabs (fn (S n) (IZR Z0))) (An (S n)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    apply H0 ; rewrite /Boule Rminus_0_r Rabs_R0 ; by apply r.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
    rewrite IH Rabs_pos_eq.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by [].
(* Goal: Rle (IZR Z0) (An (S n)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    apply Rle_trans with (Rabs (fn (S n) 0)).
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply Rabs_pos.
(* Goal: Rle (Rabs (fn (S n) (IZR Z0))) (An (S n)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    apply H0 ; rewrite /Boule Rminus_0_r Rabs_R0 ; by apply r.

(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
  have H2 : is_lim_seq (fun n => Series (fun k => An (n + k)%nat)) 0.
(* Goal: is_lim_seq (fun n : nat => Series (fun k : nat => An (Init.Nat.add n k))) (Finite (IZR Z0)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    apply is_lim_seq_incr_1.
(* Goal: is_lim_seq (fun n : nat => Series (fun k : nat => An (Init.Nat.add (S n) k))) (Finite (IZR Z0)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    apply is_lim_seq_ext with (fun n => Series An - sum_f_R0 An n).
(* Goal: forall n : nat, @eq R (Rminus (Series An) (sum_f_R0 An n)) (Series (fun k : nat => An (Init.Nat.add (S n) k))) *)
(* Goal: is_lim_seq (fun n : nat => Rminus (Series An) (sum_f_R0 An n)) (Finite (IZR Z0)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    move => n ; rewrite (Series_incr_n An (S n)) /=.
(* Goal: @eq R (Rminus (Rplus (sum_f_R0 An n) (Series (fun k : nat => An (S (Init.Nat.add n k))))) (sum_f_R0 An n)) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule An *)
(* Goal: is_lim_seq (fun n : nat => Rminus (Series An) (sum_f_R0 An n)) (Finite (IZR Z0)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    ring.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply lt_O_Sn.
(* Goal: Rlt (Rabs (Rminus (fn n x) (real (Lim_seq (fun n : nat => fn n x))))) (pos eps) *)
    by apply H1.
    replace (Finite 0) with (Rbar_plus (Series An) (- Series An))
      by (simpl ; apply Rbar_finite_eq ; ring).
(* Goal: is_lim_seq (fun n : nat => Rminus (Series An) (sum_f_R0 An n)) (Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An)))) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    apply (is_lim_seq_plus _ _ (Series An) (-Series An)).
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by apply is_lim_seq_const.
    replace (Finite (-Series An)) with (Rbar_opp (Series An))
      by (simpl ; apply Rbar_finite_eq ; ring).
(* Goal: is_lim_seq (fun n : nat => Ropp (sum_f_R0 An n)) (Rbar_opp (Finite (Series An))) *)
(* Goal: is_Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An))) (Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An)))) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    apply -> is_lim_seq_opp.
    rewrite /Series ;
    apply (is_lim_seq_ext (sum_n (fun k => An k))).
(* Goal: forall n : nat, @eq R (@sum_n R_AbelianGroup (fun k : nat => An k) n) (sum_f_R0 An n) *)
(* Goal: is_lim_seq (@sum_n R_AbelianGroup (fun k : nat => An k)) (Finite (real (Lim_seq (@sum_n R_AbelianGroup An)))) *)
(* Goal: is_Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An))) (Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An)))) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    elim => /= [ | n IH].
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by rewrite sum_O.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
    by rewrite sum_Sn IH.
(* Goal: is_lim_seq (@sum_n R_AbelianGroup (fun k : nat => An k)) (Finite (real (Lim_seq (@sum_n R_AbelianGroup An)))) *)
(* Goal: is_Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An))) (Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An)))) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    apply is_lim_seq_ext with (sum_n An).
(* Goal: forall n0 : nat, @eq (NormedModule.sort R_AbsRing R_NormedModule) (An (Init.Nat.add (S n) n0)) (An (S (Init.Nat.add n n0))) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => An (Init.Nat.add (S n) k)) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => fn k y) *)
    move => n ; by rewrite sum_n_Reals.
(* Goal: is_lim_seq (@sum_n R_AbelianGroup An) (Finite (real (Lim_seq (@sum_n R_AbelianGroup An)))) *)
(* Goal: is_Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An))) (Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An)))) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    apply Lim_seq_correct', H1.
(* Goal: is_Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An))) (Rbar_plus (Finite (Series An)) (Finite (Ropp (Series An)))) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
    easy.

(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  assert (H3 : forall y, Boule 0 r y -> ex_series (fun n => Rabs (fn n y))).
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move => y Hy.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move: H1 ; apply @ex_series_le.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (Rabs (fn n y))) (An n) *)
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  move => n.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite /norm /= /abs /= Rabs_Rabsolu.
  by apply H0.

(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  apply Rminus_lt_0 in Hx.
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  set r0 := mkposreal _ Hx.
(* Goal: @ex posreal (fun e : posreal => CVU (fun n : nat => SP fn n) (fun x : R => Series (fun n : nat => fn n x)) x e) *)
  exists r0 => e He ; set eps := mkposreal e He.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  apply is_lim_seq_spec in H2.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  case: (H2 eps) => {H2} N H2.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (y : R) (_ : le N n) (_ : Boule x r0 y), Rlt (Rabs (Rminus (Series (fun n0 : nat => fn n0 y)) (SP fn n y))) e) *)
  exists N => n y Hn Hy.

(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
  have H4 : Boule 0 r y.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite /Boule /= in Hy |- *.
(* Goal: Rlt (Rabs (Rminus y (IZR Z0))) (pos r) *)
(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
  apply Rle_lt_trans with (1 := Rabs_triang_inv _ _) in Hy.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite /Rminus ?(Rplus_comm _ (-Rabs x)) in Hy.
(* Goal: Rlt (Rabs (Rminus y (IZR Z0))) (pos r) *)
(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
  apply Rplus_lt_reg_l in Hy.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by rewrite Rminus_0_r.

(* Goal: Rlt (Rabs (Rminus (Series (fun n : nat => fn n y)) (SP fn n y))) e *)
  apply Rle_lt_trans with (2 := H2 (S n) (le_trans _ _ _ (le_n_Sn _) (le_n_S _ _ Hn))).
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite Rminus_0_r /SP.
(* Goal: Rle (Rabs (Rminus (Series (fun n : nat => fn n y)) (sum_f_R0 (fun k : nat => fn k y) n))) (Rabs (Series (fun k : nat => An (Init.Nat.add (S n) k)))) *)
  rewrite (Series_incr_n (fun k : nat => fn k y) (S n)) /=.
  ring_simplify (sum_f_R0 (fun k : nat => fn k y) n +
    Series (fun k : nat => fn (S (n + k)) y) -
    sum_f_R0 (fun k : nat => fn k y) n).

(* Goal: Rle (Rabs (Series (fun k : nat => fn (S (Init.Nat.add n k)) y))) (Rabs (Series (fun k : nat => An (S (Init.Nat.add n k))))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => fn k y) *)
  apply Rle_trans with (2 := Rle_abs _).
(* Goal: Rle (Rabs (Series (fun k : nat => fn (S (Init.Nat.add n k)) y))) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => fn k y) *)
  apply Rle_trans with (Series (fun k : nat => Rabs (fn (S (n + k)) y))).
(* Goal: Rle (Rabs (Series (fun k : nat => fn (S (Init.Nat.add n k)) y))) (Series (fun k : nat => Rabs (fn (S (Init.Nat.add n k)) y))) *)
(* Goal: Rle (Series (fun k : nat => Rabs (fn (S (Init.Nat.add n k)) y))) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => fn k y) *)
  apply Series_Rabs.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n0 : nat => Rabs (fn (S (Init.Nat.add n n0)) y)) *)
(* Goal: Rle (Series (fun k : nat => Rabs (fn (S (Init.Nat.add n k)) y))) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => fn k y) *)
  apply ex_series_ext with (fun n0 : nat => Rabs (fn (S (n) + n0)%nat y)).
(* Goal: forall n0 : nat, @eq (NormedModule.sort R_AbsRing R_NormedModule) (An (Init.Nat.add (S n) n0)) (An (S (Init.Nat.add n n0))) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => An (Init.Nat.add (S n) k)) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => fn k y) *)
    move => n0 ; by rewrite plus_Sn_m.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n0 : nat => Rabs (fn (Init.Nat.add (S n) n0) y)) *)
(* Goal: Rle (Series (fun k : nat => Rabs (fn (S (Init.Nat.add n k)) y))) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => fn k y) *)
  apply (ex_series_incr_n (fun n => Rabs (fn n y))).
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply H3.
(* Goal: Rle (Series (fun k : nat => Rabs (fn (S (Init.Nat.add n k)) y))) (Series (fun k : nat => An (S (Init.Nat.add n k)))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => fn k y) *)
  apply Series_le.
(* Goal: D_x no_cond x y *)
(* Goal: Rlt (dist R_met y x) d *)
  move => k ; split.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply Rabs_pos.
  by apply H0.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => An (S (Init.Nat.add n k))) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => fn k y) *)
  apply ex_series_ext with (fun k : nat => An (S n + k)%nat).
(* Goal: forall n0 : nat, @eq (NormedModule.sort R_AbsRing R_NormedModule) (An (Init.Nat.add (S n) n0)) (An (S (Init.Nat.add n n0))) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => An (Init.Nat.add (S n) k)) *)
(* Goal: lt O (S n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => fn k y) *)
  move => k ; by rewrite plus_Sn_m.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply ex_series_incr_n.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply lt_O_Sn.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => fn k y) *)
  apply ex_series_Rabs.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (fn n y)) *)
  by apply H3.
Qed.
