(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Ranalysis1.
Require Import MVT.
Require Import Max.
Require Import Even.
Require Import Lra.
Local Open Scope R_scope.

(* Boule is French for Ball *)

Definition Boule (x:R) (r:posreal) (y:R) : Prop := Rabs (y - x) < r.

(* General properties of balls. *)

Lemma Boule_convex : forall c d x y z,
  Boule c d x -> Boule c d y -> x <= z <= y -> Boule c d z.
forall (c : R) (d : posreal) (x y z : R),
Boule c d x ->
Boule c d y -> x <= z <= y -> Boule c d z
Proof.
forall (c : R) (d : posreal) (x y z : R),
Boule c d x ->
Boule c d y -> x <= z <= y -> Boule c d z
intros c d x y z bx b_y intz.
c:R
d:posreal
x, y, z:R
bx:Boule c d x
b_y:Boule c d y
intz:x <= z <= y
Boule c d z
unfold Boule in bx, b_y; apply Rabs_def2 in bx;
apply Rabs_def2 in b_y; apply Rabs_def1;
 [apply Rle_lt_trans with (y - c);[apply Rplus_le_compat_r|]|
  apply Rlt_le_trans with (x - c);[|apply Rplus_le_compat_r]];tauto.
Qed.

Definition boule_of_interval x y (h : x < y) :
  {c :R & {r : posreal | c - r = x /\ c + r = y}}.
x, y:R
h:x < y
{c : R & {r : posreal | c - r = x /\ c + r = y}}
Proof.
x, y:R
h:x < y
{c : R & {r : posreal | c - r = x /\ c + r = y}}
exists ((x + y)/2).
x, y:R
h:x < y
{r : posreal |
(x + y) / 2 - r = x /\ (x + y) / 2 + r = y}
assert (radius : 0 < (y - x)/2).
x, y:R
h:x < y
0 < (y - x) / 2
x, y:R
h:x < y
radius:0 < (y - x) / 2
{r : posreal |
(x + y) / 2 - r = x /\ (x + y) / 2 + r = y}
 unfold Rdiv; apply Rmult_lt_0_compat.
x, y:R
h:x < y
0 < y - x
x, y:R
h:x < y
0 < / 2
x, y:R
h:x < y
radius:0 < (y - x) / 2
{r : posreal |
(x + y) / 2 - r = x /\ (x + y) / 2 + r = y}
  apply Rlt_Rminus; assumption.
x, y:R
h:x < y
0 < / 2
x, y:R
h:x < y
radius:0 < (y - x) / 2
{r : posreal |
(x + y) / 2 - r = x /\ (x + y) / 2 + r = y}
 now apply Rinv_0_lt_compat, Rlt_0_2.
x, y:R
h:x < y
radius:0 < (y - x) / 2
{r : posreal |
(x + y) / 2 - r = x /\ (x + y) / 2 + r = y}
 exists (mkposreal _ radius).
x, y:R
h:x < y
radius:0 < (y - x) / 2
(x + y) / 2 -
{| pos := (y - x) / 2; cond_pos := radius |} = x /\
(x + y) / 2 +
{| pos := (y - x) / 2; cond_pos := radius |} = y
 simpl; split; unfold Rdiv; field.
Qed.

Definition boule_in_interval x y z (h : x < z < y) :
  {c : R & {r | Boule c r z /\  x < c - r /\ c + r < y}}.
x, y, z:R
h:x < z < y
{c : R &
{r : posreal | Boule c r z /\ x < c - r /\ c + r < y}}
Proof.
x, y, z:R
h:x < z < y
{c : R &
{r : posreal | Boule c r z /\ x < c - r /\ c + r < y}}
assert (cmp : x * /2 + z * /2 < z * /2 + y * /2).
x, y, z:R
h:x < z < y
x * / 2 + z * / 2 < z * / 2 + y * / 2
x, y, z:R
h:x < z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
{c : R &
{r : posreal | Boule c r z /\ x < c - r /\ c + r < y}}
destruct h as [h1 h2].
x, y, z:R
h1:x < z
h2:z < y
x * / 2 + z * / 2 < z * / 2 + y * / 2
x, y, z:R
h:x < z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
{c : R &
{r : posreal | Boule c r z /\ x < c - r /\ c + r < y}}
rewrite Rplus_comm; apply Rplus_lt_compat_l, Rmult_lt_compat_r.
x, y, z:R
h1:x < z
h2:z < y
0 < / 2
x, y, z:R
h1:x < z
h2:z < y
x < y
x, y, z:R
h:x < z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
{c : R &
{r : posreal | Boule c r z /\ x < c - r /\ c + r < y}}
 apply Rinv_0_lt_compat, Rlt_0_2.
x, y, z:R
h1:x < z
h2:z < y
x < y
x, y, z:R
h:x < z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
{c : R &
{r : posreal | Boule c r z /\ x < c - r /\ c + r < y}}
apply Rlt_trans with z; assumption.
x, y, z:R
h:x < z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
{c : R &
{r : posreal | Boule c r z /\ x < c - r /\ c + r < y}}
destruct (boule_of_interval _ _ cmp) as [c [r [P1 P2]]].
x, y, z:R
h:x < z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
{c0 : R &
{r0 : posreal |
Boule c0 r0 z /\ x < c0 - r0 /\ c0 + r0 < y}}
assert (0 < /2) by (apply Rinv_0_lt_compat, Rlt_0_2).
x, y, z:R
h:x < z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
{c0 : R &
{r0 : posreal |
Boule c0 r0 z /\ x < c0 - r0 /\ c0 + r0 < y}}
exists c, r; split.
x, y, z:R
h:x < z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
Boule c r z
x, y, z:R
h:x < z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
x < c - r /\ c + r < y
 destruct h; unfold Boule; simpl; apply Rabs_def1.
x, y, z:R
H0:x < z
H1:z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
z - c < r
x, y, z:R
H0:x < z
H1:z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
- r < z - c
x, y, z:R
h:x < z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
x < c - r /\ c + r < y
  apply Rplus_lt_reg_l with c; rewrite P2;
  replace (c + (z - c)) with (z * / 2 + z * / 2) by field.
x, y, z:R
H0:x < z
H1:z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
z * / 2 + z * / 2 < z * / 2 + y * / 2
x, y, z:R
H0:x < z
H1:z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
- r < z - c
x, y, z:R
h:x < z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
x < c - r /\ c + r < y
  apply Rplus_lt_compat_l, Rmult_lt_compat_r;assumption.
x, y, z:R
H0:x < z
H1:z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
- r < z - c
x, y, z:R
h:x < z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
x < c - r /\ c + r < y
 apply Rplus_lt_reg_l with c; change (c + - r) with (c - r);
 rewrite P1;
 replace (c + (z - c)) with (z * / 2 + z * / 2) by field.
x, y, z:R
H0:x < z
H1:z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
x * / 2 + z * / 2 < z * / 2 + z * / 2
x, y, z:R
h:x < z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
x < c - r /\ c + r < y
 apply Rplus_lt_compat_r, Rmult_lt_compat_r;assumption.
x, y, z:R
h:x < z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
x < c - r /\ c + r < y
destruct h; split.
x, y, z:R
H0:x < z
H1:z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
x < c - r
x, y, z:R
H0:x < z
H1:z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
c + r < y
 replace x with (x * / 2 + x * / 2) by field; rewrite P1.
x, y, z:R
H0:x < z
H1:z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
x * / 2 + x * / 2 < x * / 2 + z * / 2
x, y, z:R
H0:x < z
H1:z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
c + r < y
 apply Rplus_lt_compat_l, Rmult_lt_compat_r;assumption.
x, y, z:R
H0:x < z
H1:z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
c + r < y
replace y with (y * / 2 + y * /2) by field; rewrite P2.
x, y, z:R
H0:x < z
H1:z < y
cmp:x * / 2 + z * / 2 < z * / 2 + y * / 2
c:R
r:posreal
P1:c - r = x * / 2 + z * / 2
P2:c + r = z * / 2 + y * / 2
H:0 < / 2
z * / 2 + y * / 2 < y * / 2 + y * / 2
apply Rplus_lt_compat_r, Rmult_lt_compat_r;assumption.
Qed.

Lemma Ball_in_inter : forall c1 c2 r1 r2 x,
  Boule c1 r1 x -> Boule c2 r2 x ->
  {r3 : posreal | forall y, Boule x r3 y -> Boule c1 r1 y /\ Boule c2 r2 y}.
forall (c1 c2 : R) (r1 r2 : posreal) (x : R),
Boule c1 r1 x ->
Boule c2 r2 x ->
{r3 : posreal |
forall y : R,
Boule x r3 y -> Boule c1 r1 y /\ Boule c2 r2 y}
Proof.
forall (c1 c2 : R) (r1 r2 : posreal) (x : R),
Boule c1 r1 x ->
Boule c2 r2 x ->
{r3 : posreal |
forall y : R,
Boule x r3 y -> Boule c1 r1 y /\ Boule c2 r2 y}
intros c1 c2 [r1 r1p] [r2 r2p] x; unfold Boule; simpl; intros in1 in2.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
in1:Rabs (x - c1) < r1
in2:Rabs (x - c2) < r2
{r3 : posreal |
forall y : R,
Rabs (y - x) < r3 ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2}
assert (Rmax (c1 - r1)(c2 - r2) < x).
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
in1:Rabs (x - c1) < r1
in2:Rabs (x - c2) < r2
Rmax (c1 - r1) (c2 - r2) < x
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
in1:Rabs (x - c1) < r1
in2:Rabs (x - c2) < r2
H:Rmax (c1 - r1) (c2 - r2) < x
{r3 : posreal |
forall y : R,
Rabs (y - x) < r3 ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2}
 apply Rmax_lub_lt;[revert in1 | revert in2]; intros h;
  apply Rabs_def2 in h; destruct h as [_ u];
  apply (fun h => Rplus_lt_reg_r _ _ _ (Rle_lt_trans _ _ _ h u)), Req_le; ring.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
in1:Rabs (x - c1) < r1
in2:Rabs (x - c2) < r2
H:Rmax (c1 - r1) (c2 - r2) < x
{r3 : posreal |
forall y : R,
Rabs (y - x) < r3 ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2}
assert (x < Rmin (c1 + r1) (c2 + r2)).
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
in1:Rabs (x - c1) < r1
in2:Rabs (x - c2) < r2
H:Rmax (c1 - r1) (c2 - r2) < x
x < Rmin (c1 + r1) (c2 + r2)
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
in1:Rabs (x - c1) < r1
in2:Rabs (x - c2) < r2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
{r3 : posreal |
forall y : R,
Rabs (y - x) < r3 ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2}
 apply Rmin_glb_lt;[revert in1 | revert in2]; intros h;
 apply Rabs_def2 in h; destruct h as [u _];
 apply (fun h => Rplus_lt_reg_r _ _ _ (Rlt_le_trans _ _ _ u h)), Req_le; ring.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
in1:Rabs (x - c1) < r1
in2:Rabs (x - c2) < r2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
{r3 : posreal |
forall y : R,
Rabs (y - x) < r3 ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2}
assert (t: 0 < Rmin (x - Rmax (c1 - r1) (c2 - r2))
              (Rmin (c1 + r1) (c2 + r2) - x)).
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
in1:Rabs (x - c1) < r1
in2:Rabs (x - c2) < r2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
in1:Rabs (x - c1) < r1
in2:Rabs (x - c2) < r2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
{r3 : posreal |
forall y : R,
Rabs (y - x) < r3 ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2}
 apply Rmin_glb_lt; apply Rlt_Rminus; assumption.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
in1:Rabs (x - c1) < r1
in2:Rabs (x - c2) < r2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
{r3 : posreal |
forall y : R,
Rabs (y - x) < r3 ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2}
exists (mkposreal _ t).
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
in1:Rabs (x - c1) < r1
in2:Rabs (x - c2) < r2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
forall y : R,
Rabs (y - x) <
{|
pos := Rmin (x - Rmax (c1 - r1) (c2 - r2))
         (Rmin (c1 + r1) (c2 + r2) - x);
cond_pos := t |} ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2
apply Rabs_def2 in in1; destruct in1.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
in2:Rabs (x - c2) < r2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
forall y : R,
Rabs (y - x) <
{|
pos := Rmin (x - Rmax (c1 - r1) (c2 - r2))
         (Rmin (c1 + r1) (c2 + r2) - x);
cond_pos := t |} ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2
apply Rabs_def2 in in2; destruct in2.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
forall y : R,
Rabs (y - x) <
{|
pos := Rmin (x - Rmax (c1 - r1) (c2 - r2))
         (Rmin (c1 + r1) (c2 + r2) - x);
cond_pos := t |} ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2
assert (c1 - r1 <= Rmax (c1 - r1) (c2 - r2)) by apply Rmax_l.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
forall y : R,
Rabs (y - x) <
{|
pos := Rmin (x - Rmax (c1 - r1) (c2 - r2))
         (Rmin (c1 + r1) (c2 + r2) - x);
cond_pos := t |} ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2
assert (c2 - r2 <= Rmax (c1 - r1) (c2 - r2)) by apply Rmax_r.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
forall y : R,
Rabs (y - x) <
{|
pos := Rmin (x - Rmax (c1 - r1) (c2 - r2))
         (Rmin (c1 + r1) (c2 + r2) - x);
cond_pos := t |} ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2
assert (Rmin (c1 + r1) (c2 + r2) <= c1 + r1) by apply Rmin_l.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
forall y : R,
Rabs (y - x) <
{|
pos := Rmin (x - Rmax (c1 - r1) (c2 - r2))
         (Rmin (c1 + r1) (c2 + r2) - x);
cond_pos := t |} ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2
assert (Rmin (c1 + r1) (c2 + r2) <= c2 + r2) by apply Rmin_r.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
forall y : R,
Rabs (y - x) <
{|
pos := Rmin (x - Rmax (c1 - r1) (c2 - r2))
         (Rmin (c1 + r1) (c2 + r2) - x);
cond_pos := t |} ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2
assert (Rmin (x - Rmax (c1 - r1) (c2 - r2)) 
         (Rmin (c1 + r1) (c2 + r2) - x) <= x - Rmax (c1 - r1) (c2 - r2))
 by apply Rmin_l.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
forall y : R,
Rabs (y - x) <
{|
pos := Rmin (x - Rmax (c1 - r1) (c2 - r2))
         (Rmin (c1 + r1) (c2 + r2) - x);
cond_pos := t |} ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2
assert (Rmin (x - Rmax (c1 - r1) (c2 - r2)) 
         (Rmin (c1 + r1) (c2 + r2) - x) <= Rmin (c1 + r1) (c2 + r2) - x)
 by apply Rmin_r.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2)) (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
forall y : R,
Rabs (y - x) <
{|
pos := Rmin (x - Rmax (c1 - r1) (c2 - r2))
         (Rmin (c1 + r1) (c2 + r2) - x);
cond_pos := t |} ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2
simpl.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2)) (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
forall y : R,
Rabs (y - x) <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) ->
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2
intros y h; apply Rabs_def2 in h; destruct h as [h h'].
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2)) (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
y:R
h:y - x <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
h':-
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) < y - x
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2
apply Rmin_Rgt in h; destruct h as [cmp1 cmp2].
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2)) (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
y:R
cmp1:x - Rmax (c1 - r1) (c2 - r2) > y - x
cmp2:Rmin (c1 + r1) (c2 + r2) - x > y - x
h':-
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) < 
y - x
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2
apply Rplus_lt_reg_r in cmp2; apply Rmin_Rgt in cmp2.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
y:R
cmp1:x - Rmax (c1 - r1) (c2 - r2) > y - x
cmp2:c1 + r1 > y /\ c2 + r2 > y
h':-
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) < 
y - x
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2
rewrite Ropp_Rmin, Ropp_minus_distr in h'.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
y:R
cmp1:x - Rmax (c1 - r1) (c2 - r2) > y - x
cmp2:c1 + r1 > y /\ c2 + r2 > y
h':Rmax (Rmax (c1 - r1) (c2 - r2) - x)
  (- (Rmin (c1 + r1) (c2 + r2) - x)) < 
y - x
Rabs (y - c1) < r1 /\ Rabs (y - c2) < r2
apply Rmax_Rlt in h'; destruct h' as [cmp3 cmp4];
apply Rplus_lt_reg_r in cmp3; apply Rmax_Rlt in cmp3;
split; apply Rabs_def1.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
y:R
cmp1:x - Rmax (c1 - r1) (c2 - r2) > y - x
cmp2:c1 + r1 > y /\ c2 + r2 > y
cmp3:c1 - r1 < y /\ c2 - r2 < y
cmp4:- (Rmin (c1 + r1) (c2 + r2) - x) < y - x
y - c1 < r1
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
y:R
cmp1:x - Rmax (c1 - r1) (c2 - r2) > y - x
cmp2:c1 + r1 > y /\ c2 + r2 > y
cmp3:c1 - r1 < y /\ c2 - r2 < y
cmp4:- (Rmin (c1 + r1) (c2 + r2) - x) < y - x
- r1 < y - c1
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
y:R
cmp1:x - Rmax (c1 - r1) (c2 - r2) > y - x
cmp2:c1 + r1 > y /\ c2 + r2 > y
cmp3:c1 - r1 < y /\ c2 - r2 < y
cmp4:- (Rmin (c1 + r1) (c2 + r2) - x) < y - x
y - c2 < r2
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
y:R
cmp1:x - Rmax (c1 - r1) (c2 - r2) > y - x
cmp2:c1 + r1 > y /\ c2 + r2 > y
cmp3:c1 - r1 < y /\ c2 - r2 < y
cmp4:- (Rmin (c1 + r1) (c2 + r2) - x) < y - x
- r2 < y - c2
apply (fun h => Rplus_lt_reg_l _ _ _ (Rle_lt_trans _ _ _ h (proj1 cmp2))), Req_le;
 ring.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
y:R
cmp1:x - Rmax (c1 - r1) (c2 - r2) > y - x
cmp2:c1 + r1 > y /\ c2 + r2 > y
cmp3:c1 - r1 < y /\ c2 - r2 < y
cmp4:- (Rmin (c1 + r1) (c2 + r2) - x) < y - x
- r1 < y - c1
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
y:R
cmp1:x - Rmax (c1 - r1) (c2 - r2) > y - x
cmp2:c1 + r1 > y /\ c2 + r2 > y
cmp3:c1 - r1 < y /\ c2 - r2 < y
cmp4:- (Rmin (c1 + r1) (c2 + r2) - x) < y - x
y - c2 < r2
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
y:R
cmp1:x - Rmax (c1 - r1) (c2 - r2) > y - x
cmp2:c1 + r1 > y /\ c2 + r2 > y
cmp3:c1 - r1 < y /\ c2 - r2 < y
cmp4:- (Rmin (c1 + r1) (c2 + r2) - x) < y - x
- r2 < y - c2
apply (fun h => Rplus_lt_reg_l _ _ _ (Rlt_le_trans _ _ _ (proj1 cmp3) h)), Req_le;
 ring.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
y:R
cmp1:x - Rmax (c1 - r1) (c2 - r2) > y - x
cmp2:c1 + r1 > y /\ c2 + r2 > y
cmp3:c1 - r1 < y /\ c2 - r2 < y
cmp4:- (Rmin (c1 + r1) (c2 + r2) - x) < y - x
y - c2 < r2
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
y:R
cmp1:x - Rmax (c1 - r1) (c2 - r2) > y - x
cmp2:c1 + r1 > y /\ c2 + r2 > y
cmp3:c1 - r1 < y /\ c2 - r2 < y
cmp4:- (Rmin (c1 + r1) (c2 + r2) - x) < y - x
- r2 < y - c2
apply (fun h => Rplus_lt_reg_l _ _ _ (Rle_lt_trans _ _ _ h (proj2 cmp2))), Req_le;
 ring.
c1, c2, r1:R
r1p:0 < r1
r2:R
r2p:0 < r2
x:R
H1:x - c1 < r1
H2:- r1 < x - c1
H3:x - c2 < r2
H4:- r2 < x - c2
H:Rmax (c1 - r1) (c2 - r2) < x
H0:x < Rmin (c1 + r1) (c2 + r2)
t:0 <
Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x)
H5:c1 - r1 <= Rmax (c1 - r1) (c2 - r2)
H6:c2 - r2 <= Rmax (c1 - r1) (c2 - r2)
H7:Rmin (c1 + r1) (c2 + r2) <= c1 + r1
H8:Rmin (c1 + r1) (c2 + r2) <= c2 + r2
H9:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
x - Rmax (c1 - r1) (c2 - r2)
H10:Rmin (x - Rmax (c1 - r1) (c2 - r2))
  (Rmin (c1 + r1) (c2 + r2) - x) <=
Rmin (c1 + r1) (c2 + r2) - x
y:R
cmp1:x - Rmax (c1 - r1) (c2 - r2) > y - x
cmp2:c1 + r1 > y /\ c2 + r2 > y
cmp3:c1 - r1 < y /\ c2 - r2 < y
cmp4:- (Rmin (c1 + r1) (c2 + r2) - x) < y - x
- r2 < y - c2
apply (fun h => Rplus_lt_reg_l _ _ _ (Rlt_le_trans _ _ _ (proj2 cmp3) h)), Req_le;
 ring.
Qed.

Lemma Boule_center : forall x r, Boule x r x.
forall (x : R) (r : posreal), Boule x r x
Proof.
forall (x : R) (r : posreal), Boule x r x
intros x [r rpos]; unfold Boule, Rminus; simpl; rewrite Rplus_opp_r.
x, r:R
rpos:0 < r
Rabs 0 < r
rewrite Rabs_pos_eq;[assumption | apply Rle_refl].
Qed.

Definition CVU (fn:nat -> R -> R) (f:R -> R) (x:R)
  (r:posreal) : Prop :=
  forall eps:R,
    0 < eps ->
    exists N : nat,
      (forall (n:nat) (y:R),
        (N <= n)%nat -> Boule x r y -> Rabs (f y - fn n y) < eps).

Definition CVN_r (fn:nat -> R -> R) (r:posreal) : Type :=
  { An:nat -> R &
    { l:R |
      Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (An k)) n) l /\
      (forall (n:nat) (y:R), Boule 0 r y -> Rabs (fn n y) <= An n) } }.

Definition CVN_R (fn:nat -> R -> R) : Type := forall r:posreal, CVN_r fn r.

Definition SFL (fn:nat -> R -> R)
  (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l })
  (y:R) : R := let (a,_) := cv y in a.

Lemma CVN_CVU :
  forall (fn:nat -> R -> R)
    (cv:forall x:R, {l:R | Un_cv (fun N:nat => SP fn N x) l })
    (r:posreal), CVN_r fn r -> CVU (fun n:nat => SP fn n) (SFL fn cv) 0 r.
forall (fn : nat -> R -> R)
  (cv : forall x : R,
        {l : R | Un_cv (fun N : nat => SP fn N x) l})
  (r : posreal),
CVN_r fn r ->
CVU (fun n : nat => SP fn n) (SFL fn cv) 0 r
Proof.
forall (fn : nat -> R -> R)
  (cv : forall x : R,
        {l : R | Un_cv (fun N : nat => SP fn N x) l})
  (r : posreal),
CVN_r fn r ->
CVU (fun n : nat => SP fn n) (SFL fn cv) 0 r
  intros; unfold CVU; intros.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:CVN_r fn r
eps:R
H:0 < eps
exists N : nat,
  forall (n : nat) (y : R),
  (N <= n)%nat ->
  Boule 0 r y -> Rabs (SFL fn cv y - SP fn n y) < eps
  unfold CVN_r in X.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}}
eps:R
H:0 < eps
exists N : nat,
  forall (n : nat) (y : R),
  (N <= n)%nat ->
  Boule 0 r y -> Rabs (SFL fn cv y - SP fn n y) < eps
  elim X; intros An X0.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
exists N : nat,
  forall (n : nat) (y : R),
  (N <= n)%nat ->
  Boule 0 r y -> Rabs (SFL fn cv y - SP fn n y) < eps
  elim X0; intros s H0.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
exists N : nat,
  forall (n : nat) (y : R),
  (N <= n)%nat ->
  Boule 0 r y -> Rabs (SFL fn cv y - SP fn n y) < eps
  elim H0; intros.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
exists N : nat,
  forall (n : nat) (y : R),
  (N <= n)%nat ->
  Boule 0 r y -> Rabs (SFL fn cv y - SP fn n y) < eps
  cut (Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (An k)) n - s) 0).
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0 ->
exists N : nat,
  forall (n : nat) (y : R),
  (N <= n)%nat ->
  Boule 0 r y -> Rabs (SFL fn cv y - SP fn n y) < eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  intro; unfold Un_cv in H3.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n : nat,
  (n >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n - s)
    0 < eps0
exists N : nat,
  forall (n : nat) (y : R),
  (N <= n)%nat ->
  Boule 0 r y -> Rabs (SFL fn cv y - SP fn n y) < eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  elim (H3 eps H); intros N0 H4.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n : nat,
  (n >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n - s)
    0 < eps0
N0:nat
H4:forall n : nat,
(n >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0 <
eps
exists N : nat,
  forall (n : nat) (y : R),
  (N <= n)%nat ->
  Boule 0 r y -> Rabs (SFL fn cv y - SP fn n y) < eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  exists N0; intros.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (SFL fn cv y - SP fn n y) < eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  apply Rle_lt_trans with (Rabs (sum_f_R0 (fun k:nat => Rabs (An k)) n - s)).
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (SFL fn cv y - SP fn n y) <=
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s)
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  rewrite <- (Rabs_Ropp (sum_f_R0 (fun k:nat => Rabs (An k)) n - s));
    rewrite Ropp_minus_distr';
      rewrite (Rabs_right (s - sum_f_R0 (fun k:nat => Rabs (An k)) n)).
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (SFL fn cv y - SP fn n y) <=
s - sum_f_R0 (fun k : nat => Rabs (An k)) n
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
s - sum_f_R0 (fun k : nat => Rabs (An k)) n >= 0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  eapply sum_maj1.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Un_cv (fun n0 : nat => SP fn n0 y) (SFL fn cv y)
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
forall n0 : nat, Rabs (fn n0 y) <= Rabs (An n0)
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
s - sum_f_R0 (fun k : nat => Rabs (An k)) n >= 0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  unfold SFL; case (cv y); intro.
fn:nat -> R -> R
cv:forall x0 : R,
{l : R | Un_cv (fun N : nat => SP fn N x0) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
x:R
Un_cv (fun N : nat => SP fn N y) x ->
Un_cv (fun n0 : nat => SP fn n0 y) x
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
forall n0 : nat, Rabs (fn n0 y) <= Rabs (An n0)
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
s - sum_f_R0 (fun k : nat => Rabs (An k)) n >= 0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  trivial.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
forall n0 : nat, Rabs (fn n0 y) <= Rabs (An n0)
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
s - sum_f_R0 (fun k : nat => Rabs (An k)) n >= 0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  apply H1.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
forall n0 : nat, Rabs (fn n0 y) <= Rabs (An n0)
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
s - sum_f_R0 (fun k : nat => Rabs (An k)) n >= 0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  intro; elim H0; intros.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n1) l /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An0 n1)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) l /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1)}
s:R
H0:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1)
H1:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s
H2:forall (n1 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n1 : nat,
  (n1 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n1 - s)
    0 < eps0
N0:nat
H4:forall n1 : nat,
(n1 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n1 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
n0:nat
H7:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s
H8:forall (n1 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1
Rabs (fn n0 y) <= Rabs (An n0)
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
s - sum_f_R0 (fun k : nat => Rabs (An k)) n >= 0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  rewrite (Rabs_right (An n0)).
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n1) l /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An0 n1)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) l /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1)}
s:R
H0:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1)
H1:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s
H2:forall (n1 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n1 : nat,
  (n1 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n1 - s)
    0 < eps0
N0:nat
H4:forall n1 : nat,
(n1 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n1 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
n0:nat
H7:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s
H8:forall (n1 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1
Rabs (fn n0 y) <= An n0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n1) l /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An0 n1)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) l /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1)}
s:R
H0:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1)
H1:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s
H2:forall (n1 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n1 : nat,
  (n1 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n1 - s)
    0 < eps0
N0:nat
H4:forall n1 : nat,
(n1 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n1 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
n0:nat
H7:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s
H8:forall (n1 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1
An n0 >= 0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
s - sum_f_R0 (fun k : nat => Rabs (An k)) n >= 0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  apply H8; apply H6.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n1) l /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An0 n1)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) l /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1)}
s:R
H0:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1)
H1:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s
H2:forall (n1 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n1 : nat,
  (n1 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n1 - s)
    0 < eps0
N0:nat
H4:forall n1 : nat,
(n1 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n1 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
n0:nat
H7:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s
H8:forall (n1 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1
An n0 >= 0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
s - sum_f_R0 (fun k : nat => Rabs (An k)) n >= 0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  apply Rle_ge; apply Rle_trans with (Rabs (fn n0 y)).
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n1) l /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An0 n1)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) l /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1)}
s:R
H0:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1)
H1:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s
H2:forall (n1 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n1 : nat,
  (n1 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n1 - s)
    0 < eps0
N0:nat
H4:forall n1 : nat,
(n1 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n1 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
n0:nat
H7:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s
H8:forall (n1 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1
0 <= Rabs (fn n0 y)
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n1) l /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An0 n1)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) l /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1)}
s:R
H0:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1)
H1:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s
H2:forall (n1 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n1 : nat,
  (n1 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n1 - s)
    0 < eps0
N0:nat
H4:forall n1 : nat,
(n1 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n1 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
n0:nat
H7:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s
H8:forall (n1 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1
Rabs (fn n0 y) <= An n0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
s - sum_f_R0 (fun k : nat => Rabs (An k)) n >= 0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  apply Rabs_pos.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n1) l /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An0 n1)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) l /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1)}
s:R
H0:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s /\
(forall (n1 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1)
H1:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s
H2:forall (n1 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n1 : nat,
  (n1 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n1 - s)
    0 < eps0
N0:nat
H4:forall n1 : nat,
(n1 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n1 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
n0:nat
H7:Un_cv
  (fun n1 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n1) s
H8:forall (n1 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n1 y0) <= An n1
Rabs (fn n0 y) <= An n0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
s - sum_f_R0 (fun k : nat => Rabs (An k)) n >= 0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  apply H8; apply H6.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
s - sum_f_R0 (fun k : nat => Rabs (An k)) n >= 0
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  apply Rle_ge;
    apply Rplus_le_reg_l with (sum_f_R0 (fun k:nat => Rabs (An k)) n).
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
sum_f_R0 (fun k : nat => Rabs (An k)) n + 0 <=
sum_f_R0 (fun k : nat => Rabs (An k)) n +
(s - sum_f_R0 (fun k : nat => Rabs (An k)) n)
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  rewrite Rplus_0_r; unfold Rminus; rewrite (Rplus_comm s);
    rewrite <- Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_l;
      apply sum_incr.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
forall n0 : nat, 0 <= Rabs (An n0)
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  apply H1.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
forall n0 : nat, 0 <= Rabs (An n0)
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  intro; apply Rabs_pos.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
R_dist
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
  0 < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  unfold R_dist in H4; unfold Rminus in H4; rewrite Ropp_0 in H4.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
Rabs
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 + - s +
   0) < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  assert (H7 := H4 n H5).
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y0 : R),
 Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0)
H1:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s
H2:forall (n0 : nat) (y0 : R),
Boule 0 r y0 -> Rabs (fn n0 y0) <= An n0
H3:forall eps0 : R,
eps0 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s)
    0 < eps0
N0:nat
H4:forall n0 : nat,
(n0 >= N0)%nat ->
Rabs
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 + - s +
   0) < eps
n:nat
y:R
H5:(N0 <= n)%nat
H6:Boule 0 r y
H7:Rabs
  (sum_f_R0 (fun k : nat => Rabs (An k)) n + - s +
   0) < eps
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) <
eps
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  rewrite Rplus_0_r in H7; apply H7.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0
  unfold Un_cv in H1; unfold Un_cv; intros.
fn:nat -> R -> R
cv:forall x : R,
{l : R | Un_cv (fun N : nat => SP fn N x) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:forall eps1 : R,
eps1 > 0 ->
exists N : nat,
  forall n : nat,
  (n >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n) s <
  eps1
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
eps0:R
H3:eps0 > 0
exists N : nat,
  forall n : nat,
  (n >= N)%nat ->
  R_dist (sum_f_R0 (fun k : nat => Rabs (An k)) n - s)
    0 < eps0
  elim (H1 _ H3); intros.
fn:nat -> R -> R
cv:forall x0 : R,
{l : R | Un_cv (fun N : nat => SP fn N x0) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An0 n)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) l /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)}
s:R
H0:Un_cv
  (fun n : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n) s /\
(forall (n : nat) (y : R),
 Boule 0 r y -> Rabs (fn n y) <= An n)
H1:forall eps1 : R,
eps1 > 0 ->
exists N : nat,
  forall n : nat,
  (n >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n) s <
  eps1
H2:forall (n : nat) (y : R),
Boule 0 r y -> Rabs (fn n y) <= An n
eps0:R
H3:eps0 > 0
x:nat
H4:forall n : nat,
(n >= x)%nat ->
R_dist (sum_f_R0 (fun k : nat => Rabs (An k)) n)
  s < eps0
exists N : nat,
  forall n : nat,
  (n >= N)%nat ->
  R_dist (sum_f_R0 (fun k : nat => Rabs (An k)) n - s)
    0 < eps0
  exists x; intros.
fn:nat -> R -> R
cv:forall x0 : R,
{l : R | Un_cv (fun N : nat => SP fn N x0) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y : R),
 Boule 0 r y -> Rabs (fn n0 y) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y : R),
 Boule 0 r y -> Rabs (fn n0 y) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y : R),
 Boule 0 r y -> Rabs (fn n0 y) <= An n0)
H1:forall eps1 : R,
eps1 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0) s <
  eps1
H2:forall (n0 : nat) (y : R),
Boule 0 r y -> Rabs (fn n0 y) <= An n0
eps0:R
H3:eps0 > 0
x:nat
H4:forall n0 : nat,
(n0 >= x)%nat ->
R_dist (sum_f_R0 (fun k : nat => Rabs (An k)) n0)
  s < eps0
n:nat
H5:(n >= x)%nat
R_dist (sum_f_R0 (fun k : nat => Rabs (An k)) n - s) 0 <
eps0
  unfold R_dist; unfold R_dist in H4.
fn:nat -> R -> R
cv:forall x0 : R,
{l : R | Un_cv (fun N : nat => SP fn N x0) l}
r:posreal
X:{An0 : nat -> R &
{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An0 k)) n0) l /\
(forall (n0 : nat) (y : R),
 Boule 0 r y -> Rabs (fn n0 y) <= An0 n0)}}
eps:R
H:0 < eps
An:nat -> R
X0:{l : R |
Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) l /\
(forall (n0 : nat) (y : R),
 Boule 0 r y -> Rabs (fn n0 y) <= An n0)}
s:R
H0:Un_cv
  (fun n0 : nat =>
   sum_f_R0 (fun k : nat => Rabs (An k)) n0) s /\
(forall (n0 : nat) (y : R),
 Boule 0 r y -> Rabs (fn n0 y) <= An n0)
H1:forall eps1 : R,
eps1 > 0 ->
exists N : nat,
  forall n0 : nat,
  (n0 >= N)%nat ->
  R_dist
    (sum_f_R0 (fun k : nat => Rabs (An k)) n0) s <
  eps1
H2:forall (n0 : nat) (y : R),
Boule 0 r y -> Rabs (fn n0 y) <= An n0
eps0:R
H3:eps0 > 0
x:nat
H4:forall n0 : nat,
(n0 >= x)%nat ->
Rabs
  (sum_f_R0 (fun k : nat => Rabs (An k)) n0 - s) <
eps0
n:nat
H5:(n >= x)%nat
Rabs (sum_f_R0 (fun k : nat => Rabs (An k)) n - s - 0) <
eps0
  rewrite Rminus_0_r; apply H4; assumption.
Qed.