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

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

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

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

Require Import Reals Omega Psatz.
Require Import mathcomp.ssreflect.ssreflect.
Require Import Rcomplements.
Require Import Lim_seq Rbar Hierarchy.

(** This file gives definitions and properties about series defined on
a normed module. An equivalence with the standard library and several
convergence criteria are provided. *)

Section Definitions.

(** * Definitions *)

Context {K : AbsRing} {V : NormedModule K}.

Definition is_series (a : nat -> V) (l : V) :=
   filterlim (sum_n a) (eventually) (locally l).

Definition ex_series (a : nat -> V) :=
   exists l : V, is_series a l.

Definition Cauchy_series (a : nat -> V) :=
  forall eps : posreal,
    exists N : nat, forall n m : nat,
      (N <= n)%nat -> (N <= m)%nat ->
      norm (sum_n_m a n m) < eps.

End Definitions.

Definition Series (a : nat -> R) : R :=
   real (Lim_seq (sum_n a)).

Lemma ex_series_dec (a : nat -> R) :
  {ex_series a} + {~ ex_series a}.
Proof.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: (ex_lim_seq_dec (sum_n a)) => H.
(* Goal: sumbool (@ex_series R_AbsRing R_NormedModule a) (not (@ex_series R_AbsRing R_NormedModule a)) *)
(* Goal: sumbool (@ex_series R_AbsRing R_NormedModule a) (not (@ex_series R_AbsRing R_NormedModule a)) *)
  apply Lim_seq_correct in H.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: (Lim_seq (sum_n a)) H => [l | | ] H.
(* Goal: sumbool (@ex_series R_AbsRing R_NormedModule a) (not (@ex_series R_AbsRing R_NormedModule a)) *)
(* Goal: sumbool (@ex_series R_AbsRing R_NormedModule a) (not (@ex_series R_AbsRing R_NormedModule a)) *)
(* Goal: sumbool (@ex_series R_AbsRing R_NormedModule a) (not (@ex_series R_AbsRing R_NormedModule a)) *)
(* Goal: sumbool (@ex_series R_AbsRing R_NormedModule a) (not (@ex_series R_AbsRing R_NormedModule a)) *)
  left ; by exists l.
(* Goal: sumbool (@ex_series R_AbsRing R_NormedModule a) (not (@ex_series R_AbsRing R_NormedModule a)) *)
  right ; case => l H0.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  absurd (p_infty = Finite l) => //.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite -(is_lim_seq_unique _ _ H).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply is_lim_seq_unique.
(* Goal: sumbool (@ex_series R_AbsRing R_NormedModule a) (not (@ex_series R_AbsRing R_NormedModule a)) *)
  right ; case => l H0.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  absurd (m_infty = Finite l) => //.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite -(is_lim_seq_unique _ _ H).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply is_lim_seq_unique.
(* Goal: sumbool (@ex_series R_AbsRing R_NormedModule a) (not (@ex_series R_AbsRing R_NormedModule a)) *)
  right ; case => l.
(* Goal: forall _ : @is_series R_AbsRing R_NormedModule a l, False *)
  contradict H.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by exists l.
Qed.

Lemma is_series_unique (a : nat -> R) (l : R) :
  is_series a l -> Series a = l.
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Ha.
(* Goal: @eq (NormedModule.sort R_AbsRing R_NormedModule) (real (Lim_seq (@sum_n R_AbelianGroup a))) l *)
  replace l with (real (Finite l)) by auto.
(* Goal: @eq R (Series a) (Series b) *)
  apply (f_equal real).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply is_lim_seq_unique.
Qed.
Lemma Series_correct (a : nat -> R) :
  ex_series a -> is_series a (Series a).
Proof.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case => l Ha.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by rewrite (is_series_unique a l).
Qed.

Lemma is_series_Reals (a : nat -> R) (l : R) :
  is_series a l <-> infinite_sum a l.
Proof.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  split => H.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : ge n N), Rlt (R_dist (sum_f_R0 a n) l) e) *)
(* Goal: @eq (NormedModule.sort R_AbsRing R_NormedModule) l (Series a) *)
  apply (is_lim_seq_spec _ l) in H.
(* Goal: Un_cv (fun N : nat => sum_f_R0 a N) l *)
(* Goal: @eq (NormedModule.sort R_AbsRing R_NormedModule) l (Series a) *)
  move => e He ; set eps := mkposreal e He.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: (H eps) => /= {H} N H.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  exists N => n Hn.
(* Goal: Rlt (R_dist (sum_f_R0 a n) l) e *)
(* Goal: @eq (NormedModule.sort R_AbsRing R_NormedModule) l (Series a) *)
  rewrite <- sum_n_Reals.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply (H n Hn).
(* Goal: @is_series R_AbsRing R_NormedModule a l *)
  apply (is_lim_seq_spec _ l).
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => eps.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: (H eps (cond_pos eps)) => {H} N H.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  exists N => n Hn.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite sum_n_Reals.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply (H n Hn).
Qed.

Lemma ex_series_Reals_0 (a : nat -> R) :
  ex_series a -> { l:R | Un_cv (fun N:nat => sum_f_R0 a N) l }.
Proof.
  move => H ;
  exists (Series a) ; case: H => l H.
(* Goal: Un_cv (fun N : nat => sum_f_R0 a N) (Series a) *)
  replace (Series a) with l.
(* Goal: Un_cv (fun N : nat => sum_f_R0 a N) l *)
(* Goal: @eq (NormedModule.sort R_AbsRing R_NormedModule) l (Series a) *)
  move => e He ; set eps := mkposreal e He.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : ge n N), Rlt (R_dist (sum_f_R0 a n) l) e) *)
(* Goal: @eq (NormedModule.sort R_AbsRing R_NormedModule) l (Series a) *)
  apply (is_lim_seq_spec _ l) in H.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: (H eps) => /= {H} N H.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  exists N => n Hn.
(* Goal: Rlt (R_dist (sum_f_R0 a n) l) e *)
(* Goal: @eq (NormedModule.sort R_AbsRing R_NormedModule) l (Series a) *)
  rewrite <- sum_n_Reals.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply (H n Hn).
(* Goal: @eq (NormedModule.sort R_AbsRing R_NormedModule) l (Series a) *)
  apply sym_eq.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite /Series.
(* Goal: @eq (NormedModule.sort R_AbsRing R_NormedModule) (real (Lim_seq (@sum_n R_AbelianGroup a))) l *)
  replace l with (real (Finite l)) by auto.
(* Goal: @eq R (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (Init.Nat.add (S k) O))) (b (Init.Nat.sub (S n) (S k))))) (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (S k))) (b (Init.Nat.sub (S (S n)) (S (S k)))))) *)
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) m) (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) (S m))))) (Rplus (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) m) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p))) (Init.Nat.add (S m) (S (S n))))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
  apply f_equal.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply is_lim_seq_unique.
Qed.

Lemma ex_series_Reals_1 (a : nat -> R) :
  { l:R | Un_cv (fun N:nat => sum_f_R0 a N) l } -> ex_series a.
Proof.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case => l H.
(* Goal: @ex_series R_AbsRing R_NormedModule a *)
  exists l.
(* Goal: @is_series R_AbsRing R_NormedModule a l *)
  apply (is_lim_seq_spec _ l).
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => eps.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: (H eps (cond_pos eps)) => {H} N H.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  exists N => n Hn.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite sum_n_Reals.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply (H n Hn).
Qed.

(** Cauchy *)

Lemma Cauchy_ex_series {K : AbsRing} {V : CompleteNormedModule K}
  (a : nat -> V) :
  ex_series a -> Cauchy_series a.
Proof.
(* Goal: forall _ : @ex_series K (CompleteNormedModule.NormedModule K V) a, @Cauchy_series K (CompleteNormedModule.NormedModule K V) a *)
intros [l Hl] eps.
(* Goal: @ex nat (fun N : nat => forall (n m : nat) (_ : le N n) (_ : le N m), Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a n m)) (pos eps)) *)
set (eps' := eps / (norm_factor (V := V))).
(* Goal: @ex nat (fun N : nat => forall (n m : nat) (_ : le N n) (_ : le N m), Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a n m)) (pos eps)) *)
assert (He: 0 < eps').
(* Goal: Rlt (IZR Z0) (Rdiv (Rminus l (IZR (Zpos xH))) (IZR (Zpos (xO xH)))) *)
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  apply Rdiv_lt_0_compat.
(* Goal: Rlt (IZR Z0) (pos eps) *)
(* Goal: Rlt (IZR Z0) (@norm_factor K (CompleteNormedModule.NormedModule K V)) *)
(* Goal: @ex nat (fun N : nat => forall (n m : nat) (_ : le N n) (_ : le N m), Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a n m)) (pos eps)) *)
  apply eps.
(* Goal: Rlt (IZR Z0) (@norm_factor K (CompleteNormedModule.NormedModule K V)) *)
(* Goal: @ex nat (fun N : nat => forall (n m : nat) (_ : le N n) (_ : le N m), Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a n m)) (pos eps)) *)
  apply norm_factor_gt_0.
destruct (proj2 (filterlim_locally_cauchy (U := V) (F := eventually) (sum_n (fun k => a k)))
  (ex_intro _ l Hl) (mkposreal _ He)) as [P [[N HN] HP]].
(* Goal: @ex nat (fun N : nat => forall (n m : nat) (_ : le N n) (_ : le N m), Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a n m)) (pos eps)) *)
exists (S N).
(* Goal: forall (n m : nat) (_ : le (S N) n) (_ : le (S N) m), Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a n m)) (pos eps) *)
intros [|u] v Hu Hv.
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a O v)) (pos eps) *)
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a (S u) v)) (pos eps) *)
elim le_Sn_O with (1 := Hu).
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a (S u) v)) (pos eps) *)
destruct (le_or_lt u v) as [Huv|Huv].
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a (S u) v)) (pos eps) *)
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a (S u) v)) (pos eps) *)
rewrite -> sum_n_m_sum_n with (1 := Huv).
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@minus (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) (@sum_n (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a v) (@sum_n (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a u))) (pos eps) *)
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a (S u) v)) (pos eps) *)
replace (pos eps) with (norm_factor (V := V) * mkposreal _ He).
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@minus (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) (@sum_n (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a v) (@sum_n (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a u))) (Rmult (@norm_factor K (CompleteNormedModule.NormedModule K V)) (pos (mkposreal eps' He))) *)
(* Goal: @eq R (Rmult (@norm_factor K (CompleteNormedModule.NormedModule K V)) (pos (mkposreal eps' He))) (pos eps) *)
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a (S u) v)) (pos eps) *)
apply norm_compat2.
(* Goal: @ball (NormedModule.UniformSpace K (CompleteNormedModule.NormedModule K V)) (@sum_n (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a u) (pos (mkposreal eps' He)) (@sum_n (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a v) *)
(* Goal: @eq R (Rmult (@norm_factor K (CompleteNormedModule.NormedModule K V)) (pos (mkposreal eps' He))) (pos eps) *)
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a (S u) v)) (pos eps) *)
apply HP ; apply HN.
(* Goal: le N u *)
(* Goal: le N v *)
(* Goal: @eq R (Rmult (@norm_factor K (CompleteNormedModule.NormedModule K V)) (pos (mkposreal eps' He))) (pos eps) *)
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a (S u) v)) (pos eps) *)
now apply le_S_n.
(* Goal: le N v *)
(* Goal: @eq R (Rmult (@norm_factor K (CompleteNormedModule.NormedModule K V)) (pos (mkposreal eps' He))) (pos eps) *)
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a (S u) v)) (pos eps) *)
now apply le_Sn_le.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
rewrite /eps' /=.
(* Goal: @eq R (Rmult (@norm_factor K (CompleteNormedModule.NormedModule K V)) (Rdiv (pos eps) (@norm_factor K (CompleteNormedModule.NormedModule K V)))) (pos eps) *)
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a (S u) v)) (pos eps) *)
field.
(* Goal: not (@eq R (@norm_factor K (CompleteNormedModule.NormedModule K V)) (IZR Z0)) *)
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a (S u) v)) (pos eps) *)
apply Rgt_not_eq, norm_factor_gt_0.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
rewrite sum_n_m_zero.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
rewrite norm_zero.
(* Goal: Rlt (IZR Z0) (pos eps) *)
(* Goal: lt v (S u) *)
apply cond_pos.
(* Goal: lt v (S u) *)
now apply lt_S.
Qed.

Lemma ex_series_Cauchy {K : AbsRing} {V : CompleteNormedModule K}
  (a : nat -> V) :
  Cauchy_series a -> ex_series a.
Proof.
intros Ca.
destruct (proj1 (filterlim_locally_cauchy (U := V) (F := eventually) (sum_n a))) as [l Hl].
(* Goal: @ex_series R_AbsRing R_NormedModule a *)
2: now exists l.
(* Goal: is_lim_seq' a (Finite (IZR Z0)) *)
intros eps.
destruct (Ca eps) as [N HN].
exists (le N).
split.
now exists N.
intros u v.
wlog Huv: u v / (u <= v)%nat.
(* Goal: forall _ : @is_series K V (fun k : nat => a (S k)) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O))), @is_series K V a l *)
intros H.
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a (S u) v)) (pos eps) *)
destruct (le_or_lt u v) as [Huv|Huv].
now apply H.
intros Hu Hv.
apply ball_sym.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
apply H => //.
now apply lt_le_weak.
intros Hu Hv.
(* Goal: @eq (NormedModule.sort K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a n) (a (S n)))) (@plus (NormedModule.AbelianGroup K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@sum_n (NormedModule.AbelianGroup K V) a n)) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (a (S n)))) *)
(* Goal: @filterlim nat (ModuleSpace.sort (AbsRing.Ring K) (NormedModule.ModuleSpace K V)) (fun n : nat => @scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@sum_n (NormedModule.AbelianGroup K V) a n)) eventually (@locally (NormedModule.UniformSpace K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c l)) *)
apply: norm_compat1.
rewrite <- sum_n_m_sum_n with (1 := Huv).
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
apply HN => //.
now apply le_S.
Qed.

Section Properties1.

Context {K : AbsRing} {V : NormedModule K}.

(** Extensionality *)

Lemma is_series_ext (a b : nat -> V) (l : V) :
  (forall n, a n = b n) -> (is_series a l)
    -> is_series b l.
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Heq.
(* Goal: forall _ : @is_series K V a l, @is_series K V b l *)
  apply filterlim_ext.
(* Goal: forall x : nat, @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@sum_n (NormedModule.AbelianGroup K V) a x) (@sum_n (NormedModule.AbelianGroup K V) b x) *)
  intros x; now apply sum_n_m_ext.
Qed.
Lemma ex_series_ext (a b : nat -> V) :
  (forall n, a n = b n) -> ex_series a
    -> ex_series b.
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Heq [l Ha].
(* Goal: @ex_series K V b *)
  exists l ; by apply is_series_ext with a.
Qed.
Lemma Series_ext (a b : nat -> R) :
  (forall n, a n = b n) -> Series a = Series b.
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Heq.
(* Goal: @eq R (Series a) (Series b) *)
  apply (f_equal real).
(* Goal: @eq Rbar (Lim_seq (@sum_n R_AbelianGroup a)) (Lim_seq (@sum_n R_AbelianGroup b)) *)
  apply Lim_seq_ext.
(* Goal: forall n : nat, @eq R (@sum_n R_AbelianGroup a n) (@sum_n R_AbelianGroup b n) *)
  intros n; now apply sum_n_m_ext.
Qed.

(** Index offset *)

Lemma is_series_incr_1 (a : nat -> V) (l : V) :
  is_series a (plus l  (a O))
    -> is_series (fun k => a (S k)%nat) l.
Proof.
(* Goal: forall _ : @is_series K V (fun k : nat => a (S k)) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O))), @is_series K V a l *)
  intros H.
(* Goal: @is_series K V (fun k : nat => a (S k)) l *)
  apply filterlim_ext with (fun k => plus (sum_n a (S k)) (opp (a 0%nat))).
(* Goal: forall x : nat, @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (S x)) (@opp (NormedModule.AbelianGroup K V) (a O))) (@sum_n (NormedModule.AbelianGroup K V) (fun k : nat => a (S k)) x) *)
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun k : nat => @plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (S k)) (@opp (NormedModule.AbelianGroup K V) (a O))) eventually (@locally (NormedModule.UniformSpace K V) l) *)
  induction x; simpl.
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) l *)
  rewrite sum_Sn !sum_O (plus_comm _ (a 1%nat)); rewrite <- plus_assoc.
(* Goal: @eq nat (Init.Nat.add (S n) (S O)) (S (S n)) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
  now rewrite plus_opp_r plus_zero_r.
(* Goal: @eq (NormedModule.sort K V) (@plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (S (S x))) (@opp (NormedModule.AbelianGroup K V) (a O))) (@sum_n (NormedModule.AbelianGroup K V) (fun k : nat => a (S k)) (S x)) *)
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun k : nat => @plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (S k)) (@opp (NormedModule.AbelianGroup K V) (a O))) eventually (@locally (NormedModule.UniformSpace K V) l) *)
  rewrite !sum_Sn -IHx -!sum_Sn sum_Sn; simpl.
(* Goal: @eq (NormedModule.sort K V) (@plus (NormedModule.AbelianGroup K V) (@plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (S x)) (a (S (S x)))) (@opp (NormedModule.AbelianGroup K V) (a O))) (@plus (NormedModule.AbelianGroup K V) (@plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (S x)) (@opp (NormedModule.AbelianGroup K V) (a O))) (a (S (S x)))) *)
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun k : nat => @plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (S k)) (@opp (NormedModule.AbelianGroup K V) (a O))) eventually (@locally (NormedModule.UniformSpace K V) l) *)
  rewrite <- plus_assoc, <- (plus_assoc _ _ (a (S (S x)))).
(* Goal: @eq (NormedModule.sort K V) (@plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (S x)) (@plus (NormedModule.AbelianGroup K V) (a (S (S x))) (@opp (NormedModule.AbelianGroup K V) (a O)))) (@plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (S x)) (@plus (NormedModule.AbelianGroup K V) (@opp (NormedModule.AbelianGroup K V) (a O)) (a (S (S x))))) *)
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun k : nat => @plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (S k)) (@opp (NormedModule.AbelianGroup K V) (a O))) eventually (@locally (NormedModule.UniformSpace K V) l) *)
  apply f_equal; apply plus_comm.
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun k : nat => @plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (S k)) (@opp (NormedModule.AbelianGroup K V) (a O))) eventually (@locally (NormedModule.UniformSpace K V) l) *)
  apply filterlim_comp with (G:=(locally (plus l (a 0%nat)))) (g:=fun x => plus x (opp (a 0%nat))).
  (* . *)
(* Goal: @filterlim nat (UniformSpace.sort (NormedModule.UniformSpace K V)) (fun x : nat => @sum_n (NormedModule.AbelianGroup K V) a (S x)) eventually (@locally (NormedModule.UniformSpace K V) (@plus (NormedModule.AbelianGroup K V) l (a O))) *)
(* Goal: @filterlim (UniformSpace.sort (NormedModule.UniformSpace K V)) (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun x : AbelianGroup.sort (NormedModule.AbelianGroup K V) => @plus (NormedModule.AbelianGroup K V) x (@opp (NormedModule.AbelianGroup K V) (a O))) (@locally (NormedModule.UniformSpace K V) (@plus (NormedModule.AbelianGroup K V) l (a O))) (@locally (NormedModule.UniformSpace K V) l) *)
  apply filterlim_comp with (f:= fun x => S x) (2:=H).
(* Goal: @filterlim nat nat (fun x : nat => S x) eventually eventually *)
(* Goal: @filterlim (UniformSpace.sort (NormedModule.UniformSpace K V)) (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun x : AbelianGroup.sort (NormedModule.AbelianGroup K V) => @plus (NormedModule.AbelianGroup K V) x (@opp (NormedModule.AbelianGroup K V) (a O))) (@locally (NormedModule.UniformSpace K V) (@plus (NormedModule.AbelianGroup K V) l (a O))) (@locally (NormedModule.UniformSpace K V) l) *)
  apply eventually_subseq; intros n; omega.
  (* . *)
(* Goal: @filterlim (UniformSpace.sort (NormedModule.UniformSpace K V)) (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun x : AbelianGroup.sort (NormedModule.AbelianGroup K V) => @plus (NormedModule.AbelianGroup K V) x (@opp (NormedModule.AbelianGroup K V) (a O))) (@locally (NormedModule.UniformSpace K V) (@plus (NormedModule.AbelianGroup K V) l (a O))) (@locally (NormedModule.UniformSpace K V) l) *)
  pattern l at 2; replace l with (plus (plus l (a 0%nat)) (opp (a 0%nat))).
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun v : nat => @plus (NormedModule.AbelianGroup K V) (a O) (@sum_n (NormedModule.AbelianGroup K V) (fun k : nat => a (S k)) (Init.Nat.pred v))) eventually (@locally (NormedModule.UniformSpace K V) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O))))) *)
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) l *)
  apply filterlim_comp_2 with (3 := filterlim_plus _ _).
(* Goal: @filterlim nat (NormedModule.sort K V) (fun _ : nat => a O) eventually (@locally (NormedModule.UniformSpace K V) (a O)) *)
(* Goal: @filterlim nat (NormedModule.sort K V) (fun x : nat => @sum_n (NormedModule.AbelianGroup K V) (fun k : nat => a (S k)) (Init.Nat.pred x)) eventually (@locally (NormedModule.UniformSpace K V) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) *)
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) l *)
  apply filterlim_id.
(* Goal: @filterlim nat (NormedModule.sort K V) (fun _ : nat => a O) eventually (@locally (NormedModule.UniformSpace K V) (a O)) *)
(* Goal: @filterlim nat (NormedModule.sort K V) (fun x : nat => @sum_n (NormedModule.AbelianGroup K V) (fun k : nat => a (S k)) (Init.Nat.pred x)) eventually (@locally (NormedModule.UniformSpace K V) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) *)
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) l *)
  apply filterlim_const.
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (@plus (NormedModule.AbelianGroup K V) l (a O)) (@opp (NormedModule.AbelianGroup K V) (a O))) l *)
  rewrite <- plus_assoc, plus_opp_r.
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) l (@zero (NormedModule.AbelianGroup K V))) l *)
  apply plus_zero_r.
Qed.

Lemma is_series_incr_n (a : nat -> V) (n : nat) (l : V) :
  (0 < n)%nat -> is_series a (plus l (sum_n a (pred n)))
    -> is_series (fun k => a (n + k)%nat) l.
Proof.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: n => /= [ | n] Hn Ha.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply lt_irrefl in Hn.
(* Goal: @is_series K V a l *)
  clear Hn.
(* Goal: forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
  elim: n l Ha => [ | n IH] l Ha.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite sum_O in Ha.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply is_series_incr_1.
(* Goal: @is_series K V (fun k : nat => a (S (Init.Nat.add (S n) k))) l *)
  apply is_series_ext with (fun k : nat => a (S (n + S k))).
(* Goal: forall n0 : nat, @eq (NormedModule.sort K V) (a (S (Init.Nat.add n (S n0)))) (a (S (Init.Nat.add (S n) n0))) *)
(* Goal: @is_series K V (fun k : nat => a (S (Init.Nat.add n (S k)))) l *)
  move => k ; apply f_equal ; ring.
(* Goal: @is_series K V (fun k : nat => a (S (Init.Nat.add n (S k)))) l *)
  apply (is_series_incr_1 (fun k : nat => a (S (n + k))) l).
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite plus_0_r.
(* Goal: @is_series K V (fun k : nat => a (S k)) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O))) *)
  apply IH.
(* Goal: @is_series K V a (@plus (NormedModule.AbelianGroup K V) (@plus (NormedModule.AbelianGroup K V) l (a (S n))) (@sum_n (NormedModule.AbelianGroup K V) a n)) *)
  replace (plus (plus l (a (S n))) (sum_n a n)) with (plus l (sum_n a (S n))).
(* Goal: @is_series K V a (@plus (NormedModule.AbelianGroup K V) l (@sum_n (NormedModule.AbelianGroup K V) a (S n))) *)
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) l (@sum_n (NormedModule.AbelianGroup K V) a (S n))) (@plus (NormedModule.AbelianGroup K V) (@plus (NormedModule.AbelianGroup K V) l (a (S n))) (@sum_n (NormedModule.AbelianGroup K V) a n)) *)
  assumption.
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) l (@sum_n (NormedModule.AbelianGroup K V) a (S n))) (@plus (NormedModule.AbelianGroup K V) (@plus (NormedModule.AbelianGroup K V) l (a (S n))) (@sum_n (NormedModule.AbelianGroup K V) a n)) *)
  rewrite <- plus_assoc, sum_Sn; apply f_equal; simpl; apply plus_comm.
Qed.

Lemma is_series_decr_1 (a : nat -> V) (l : V) :
  is_series (fun k => a (S k)%nat) (plus l (opp (a O))) -> is_series a l.
Proof.
(* Goal: forall _ : @is_series K V (fun k : nat => a (S k)) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O))), @is_series K V a l *)
  intros H.
(* Goal: @is_series K V a l *)
  apply filterlim_ext_loc with (fun v => plus (a 0%nat) (sum_n (fun k : nat => a (S k)) (pred v))).
(* Goal: eventually (fun x : nat => @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a O) (@sum_n (NormedModule.AbelianGroup K V) (fun k : nat => a (S k)) (Init.Nat.pred x))) (@sum_n (NormedModule.AbelianGroup K V) a x)) *)
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun v : nat => @plus (NormedModule.AbelianGroup K V) (a O) (@sum_n (NormedModule.AbelianGroup K V) (fun k : nat => a (S k)) (Init.Nat.pred v))) eventually (@locally (NormedModule.UniformSpace K V) l) *)
  exists 1%nat.
(* Goal: @eq (NormedModule.sort R_AbsRing R_NormedModule) l (Series a) *)
  intros n Hn; apply sym_eq.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite /sum_n sum_Sn_m.
(* Goal: @eq R (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (Init.Nat.add (S k) O))) (b (Init.Nat.sub (S n) (S k))))) (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (S k))) (b (Init.Nat.sub (S (S n)) (S (S k)))))) *)
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) m) (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) (S m))))) (Rplus (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) m) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p))) (Init.Nat.add (S m) (S (S n))))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
  apply f_equal.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite sum_n_m_S.
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@sum_n_m (NormedModule.AbelianGroup K V) a (S O) n) (@sum_n_m (NormedModule.AbelianGroup K V) a (S O) (S (Init.Nat.pred n))) *)
(* Goal: le O n *)
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun v : nat => @plus (NormedModule.AbelianGroup K V) (a O) (@sum_n (NormedModule.AbelianGroup K V) (fun k : nat => a (S k)) (Init.Nat.pred v))) eventually (@locally (NormedModule.UniformSpace K V) l) *)
  apply f_equal ; omega.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply le_O_n.
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun v : nat => @plus (NormedModule.AbelianGroup K V) (a O) (@sum_n (NormedModule.AbelianGroup K V) (fun k : nat => a (S k)) (Init.Nat.pred v))) eventually (@locally (NormedModule.UniformSpace K V) l) *)
  replace l with (plus (a 0%nat) (plus l (opp (a 0%nat)))).
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun v : nat => @plus (NormedModule.AbelianGroup K V) (a O) (@sum_n (NormedModule.AbelianGroup K V) (fun k : nat => a (S k)) (Init.Nat.pred v))) eventually (@locally (NormedModule.UniformSpace K V) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O))))) *)
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) l *)
  apply filterlim_comp_2 with (3 := filterlim_plus _ _).
(* Goal: @filterlim nat (NormedModule.sort K V) (fun _ : nat => a O) eventually (@locally (NormedModule.UniformSpace K V) (a O)) *)
(* Goal: @filterlim nat (NormedModule.sort K V) (fun x : nat => @sum_n (NormedModule.AbelianGroup K V) (fun k : nat => a (S k)) (Init.Nat.pred x)) eventually (@locally (NormedModule.UniformSpace K V) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) *)
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) l *)
  apply filterlim_id.
(* Goal: @filterlim nat (NormedModule.sort K V) (fun _ : nat => a O) eventually (@locally (NormedModule.UniformSpace K V) (a O)) *)
(* Goal: @filterlim nat (NormedModule.sort K V) (fun x : nat => @sum_n (NormedModule.AbelianGroup K V) (fun k : nat => a (S k)) (Init.Nat.pred x)) eventually (@locally (NormedModule.UniformSpace K V) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) *)
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) l *)
  apply filterlim_const.
(* Goal: @filterlim nat (NormedModule.sort K V) (fun x : nat => @sum_n (NormedModule.AbelianGroup K V) (fun k : nat => a (S k)) (Init.Nat.pred x)) eventually (@locally (NormedModule.UniformSpace K V) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) *)
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) l *)
  apply filterlim_comp with (f:= fun x => pred x) (2:=H).
(* Goal: @filterlim nat nat (fun x : nat => Init.Nat.pred x) eventually eventually *)
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) l *)
  intros P (N1,HN1).
(* Goal: @filtermap nat nat (fun x : nat => Init.Nat.pred x) eventually P *)
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) l *)
  exists (S N1).
(* Goal: forall (n : nat) (_ : le (S N1) n), P (Init.Nat.pred n) *)
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) l *)
  intros n Hn; apply HN1; omega.
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) l *)
  rewrite plus_comm; rewrite <- plus_assoc.
(* Goal: @eq R (Rdiv (Rminus (IZR (Zpos xH)) (pow q (S n))) (Rminus (IZR (Zpos xH)) q)) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => pow q n) n) *)
(* Goal: @filterlim nat R (fun n : nat => Rdiv (Rminus (IZR (Zpos xH)) (pow q (S n))) (Rminus (IZR (Zpos xH)) q)) eventually (@locally (NormedModule.UniformSpace R_AbsRing R_NormedModule) (Rinv (Rminus (IZR (Zpos xH)) q))) *)
  rewrite (plus_comm _ (a 0%nat)); rewrite plus_opp_r.
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) l (@zero (NormedModule.AbelianGroup K V))) l *)
  apply plus_zero_r.
Qed.


Lemma is_series_decr_n (a : nat -> V) (n : nat) (l : V) :
  (0 < n)%nat -> is_series (fun k => a (n + k)%nat) (plus l (opp (sum_n a (pred n))))
    -> is_series a l.
Proof.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: n => /= [ | n] Hn Ha.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply lt_irrefl in Hn.
(* Goal: @is_series K V a l *)
  clear Hn.
(* Goal: forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
  elim: n a l Ha => [ | n IH] a l Ha.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite sum_O in Ha.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply is_series_decr_1.
(* Goal: @is_series R_AbsRing R_NormedModule a (Rplus (Series (fun k : nat => a (S k))) (a O)) *)
  apply is_series_decr_1.
(* Goal: @is_series K V (fun k : nat => a (S k)) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O))) *)
  apply IH.
  replace (plus (plus l (opp (a 0%nat))) (opp (sum_n (fun k : nat => a (S k)) n)))
    with (plus l (opp (sum_n a (S n)))).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Ha.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite /sum_n sum_n_m_S sum_Sn_m /=.
(* Goal: @eq (NormedModule.sort K V) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (@plus (NormedModule.AbelianGroup K V) (a O) (@sum_n_m (NormedModule.AbelianGroup K V) a (S O) (S n))))) (@plus (NormedModule.AbelianGroup K V) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O))) (@opp (NormedModule.AbelianGroup K V) (@sum_n_m (NormedModule.AbelianGroup K V) a (S O) (S n)))) *)
(* Goal: le O (S n) *)
  rewrite <- plus_assoc.
(* Goal: @eq R (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (Init.Nat.add (S k) O))) (b (Init.Nat.sub (S n) (S k))))) (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (S k))) (b (Init.Nat.sub (S (S n)) (S (S k)))))) *)
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) m) (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) (S m))))) (Rplus (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) m) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p))) (Init.Nat.add (S m) (S (S n))))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
  apply f_equal.
(* Goal: @eq nat (Init.Nat.add (S n) (S O)) (S (S n)) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
  now rewrite opp_plus.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply le_O_n.
Qed.

Lemma ex_series_incr_1 (a : nat -> V) :
  ex_series a <-> ex_series (fun k => a (S k)%nat).
Proof.
(* Goal: iff (@ex_series K V a) (@ex_series K V (fun k : nat => a (Init.Nat.add (S n) k))) *)
  split ; move => [la Ha].
  exists (plus la  (opp (a O))).
  apply is_series_incr_1.
(* Goal: @is_series K V a (@plus (NormedModule.AbelianGroup K V) (@plus (NormedModule.AbelianGroup K V) la (@opp (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (Init.Nat.pred (S n))))) (@sum_n (NormedModule.AbelianGroup K V) a (Init.Nat.pred (S n)))) *)
(* Goal: @ex_series K V a *)
  now rewrite <- plus_assoc, plus_opp_l, plus_zero_r.
  exists (plus la (a O)).
(* Goal: @is_series R_AbsRing R_NormedModule a (Rplus (Series (fun k : nat => a (S k))) (a O)) *)
  apply is_series_decr_1.
(* Goal: @is_series K V (fun k : nat => a (Init.Nat.add (S n) k)) (@plus (NormedModule.AbelianGroup K V) (@plus (NormedModule.AbelianGroup K V) la (@sum_n (NormedModule.AbelianGroup K V) a (Init.Nat.pred (S n)))) (@opp (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (Init.Nat.pred (S n))))) *)
  now rewrite <- plus_assoc, plus_opp_r, plus_zero_r.
Qed.

Lemma ex_series_incr_n (a : nat -> V) (n : nat) :
  ex_series a <-> ex_series (fun k => a (n + k)%nat).
Proof.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: n => [ | n].
(* Goal: iff (@ex_series K V a) (@ex_series K V (fun k : nat => a (Init.Nat.add O k))) *)
(* Goal: iff (@ex_series K V a) (@ex_series K V (fun k : nat => a (Init.Nat.add (S n) k))) *)
  split ; apply ex_series_ext ; by intuition.
(* Goal: iff (@ex_series K V a) (@ex_series K V (fun k : nat => a (Init.Nat.add (S n) k))) *)
  split ; move => [la Ha].
(* Goal: @ex_series K V (fun k : nat => a (Init.Nat.add (S n) k)) *)
(* Goal: @ex_series K V a *)
  exists (plus la (opp (sum_n a (pred (S n))))).
(* Goal: @is_series K V (fun k : nat => a (Init.Nat.add (S n) k)) (@plus (NormedModule.AbelianGroup K V) la (@opp (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (Init.Nat.pred (S n))))) *)
(* Goal: @ex_series K V a *)
  apply is_series_incr_n.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply lt_O_Sn.
(* Goal: @is_series K V a (@plus (NormedModule.AbelianGroup K V) (@plus (NormedModule.AbelianGroup K V) la (@opp (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (Init.Nat.pred (S n))))) (@sum_n (NormedModule.AbelianGroup K V) a (Init.Nat.pred (S n)))) *)
(* Goal: @ex_series K V a *)
  now rewrite <- plus_assoc, plus_opp_l, plus_zero_r.
(* Goal: @ex_series K V a *)
  exists (plus la (sum_n a (pred (S n)))).
(* Goal: @is_series K V a (@plus (NormedModule.AbelianGroup K V) la (@sum_n (NormedModule.AbelianGroup K V) a (Init.Nat.pred (S n)))) *)
  apply is_series_decr_n with (S n).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply lt_O_Sn.
(* Goal: @is_series K V (fun k : nat => a (Init.Nat.add (S n) k)) (@plus (NormedModule.AbelianGroup K V) (@plus (NormedModule.AbelianGroup K V) la (@sum_n (NormedModule.AbelianGroup K V) a (Init.Nat.pred (S n)))) (@opp (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (Init.Nat.pred (S n))))) *)
  now rewrite <- plus_assoc, plus_opp_r, plus_zero_r.
Qed.

End Properties1.

Lemma Series_incr_1 (a : nat -> R) :
  ex_series a -> Series a = a O + Series (fun k => a (S k)).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Ha.
(* Goal: @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  apply is_series_unique.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite Rplus_comm.
(* Goal: @is_series R_AbsRing R_NormedModule a (Rplus (Series (fun k : nat => a (S k))) (a O)) *)
  apply is_series_decr_1.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite /plus /opp /=.
(* Goal: @is_series R_AbsRing R_NormedModule (fun k : nat => a (S k)) (Rplus (Rplus (Series (fun k : nat => a (S k))) (a O)) (Ropp (a O))) *)
  ring_simplify (Series (fun k : nat => a (S k)) + a 0%nat +- a 0%nat).
(* Goal: @is_series R_AbsRing R_NormedModule (fun k : nat => a (Init.Nat.add n k)) (Series (fun k : nat => a (Init.Nat.add n k))) *)
  apply Series_correct.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply (ex_series_incr_1 a).
Qed.

Lemma Series_incr_n (a : nat -> R) (n : nat) :
  (0 < n)%nat -> ex_series a
    -> Series a = sum_f_R0 a (pred n)  + Series (fun k => a (n + k)%nat).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Hn Ha.
(* Goal: @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  apply is_series_unique.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite Rplus_comm.
(* Goal: @is_series R_AbsRing R_NormedModule a (Rplus (Series (fun k : nat => a (Init.Nat.add n k))) (sum_f_R0 a (Init.Nat.pred n))) *)
  apply is_series_decr_n with n.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by [].
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite /plus /opp /= sum_n_Reals.
(* Goal: @is_series R_AbsRing R_NormedModule (fun k : nat => a (Init.Nat.add n k)) (Rplus (Rplus (Series (fun k : nat => a (Init.Nat.add n k))) (sum_f_R0 a (Init.Nat.pred n))) (Ropp (sum_f_R0 a (Init.Nat.pred n)))) *)
  ring_simplify (Series (fun k : nat => a (n+ k)%nat) + sum_f_R0 a (pred n) + - sum_f_R0 a (pred n)).
(* Goal: @is_series R_AbsRing R_NormedModule (fun k : nat => a (Init.Nat.add n k)) (Series (fun k : nat => a (Init.Nat.add n k))) *)
  apply Series_correct.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply ex_series_incr_n.
Qed.

Lemma Series_incr_1_aux (a : nat -> R) :
  a O = 0 -> Series a = Series (fun k => a (S k)).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Ha.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite /Series.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite -Lim_seq_incr_1.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  apply f_equal, Lim_seq_ext => n.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite /sum_n sum_n_m_S sum_Sn_m.
(* Goal: Rle (Rmult (Rabs (a N)) (IZR (Zpos xH))) (Rabs (a N)) *)
(* Goal: Rle (Rmult (Rabs (a N)) (Rmult k (pow k n))) (Rabs (a (S (Init.Nat.add n N)))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
  rewrite Ha ; by apply Rplus_0_l.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply le_O_n.
Qed.
Lemma Series_incr_n_aux (a : nat -> R) (n : nat) :
   (forall k, (k < n)%nat -> a k = 0)
     -> Series a = Series (fun k => a (n + k)%nat).
Proof.
(* Goal: forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
  elim: n => [ | n IH] Ha.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Series_ext => k.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite IH.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite Series_incr_1_aux.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  apply Series_ext => k.
(* Goal: @eq R (a (Init.Nat.add n (S k))) (a (Init.Nat.add (S n) k)) *)
(* Goal: @eq R (a (Init.Nat.add n O)) (IZR Z0) *)
(* Goal: forall (k : nat) (_ : lt k n), @eq R (a k) (IZR Z0) *)
  apply f_equal ; ring.
(* Goal: @eq R (a (Init.Nat.add n O)) (IZR Z0) *)
(* Goal: forall (k : nat) (_ : lt k n), @eq R (a k) (IZR Z0) *)
  intuition.
(* Goal: @eq R (a (Init.Nat.add n O)) (IZR Z0) *)
(* Goal: forall (k : nat) (_ : lt k n), @eq R (a k) (IZR Z0) *)
  move => k Hk ; intuition.
Qed.

(** * Convergence theorems *)

Lemma Cauchy_series_Reals (a : nat -> R) :
  Cauchy_series a <-> Cauchy_crit_series a.
Proof.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  split => Hcv.
  apply cv_cauchy_1, ex_series_Reals_0.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply: ex_series_Cauchy.
(* Goal: @eq (NormedModule.sort K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a n) (a (S n)))) (@plus (NormedModule.AbelianGroup K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@sum_n (NormedModule.AbelianGroup K V) a n)) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (a (S n)))) *)
(* Goal: @filterlim nat (ModuleSpace.sort (AbsRing.Ring K) (NormedModule.ModuleSpace K V)) (fun n : nat => @scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@sum_n (NormedModule.AbelianGroup K V) a n)) eventually (@locally (NormedModule.UniformSpace K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c l)) *)
  apply: Cauchy_ex_series.
  apply ex_series_Reals_1.
  apply cv_cauchy_2.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Hcv.
Qed.

Lemma ex_series_lim_0 (a : nat -> R) :
  ex_series a -> is_lim_seq a 0.
Proof.
(* Goal: forall _ : @ex_series R_AbsRing R_NormedModule a, is_lim_seq a (Finite (IZR Z0)) *)
  intros Hs.
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a (Nat.div2 n)) (sum_f_R0 b (Nat.div2 n))) (Rbar_mult (Finite la) (Finite lb)) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Rbar_mult (Finite la) (Finite lb)) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Finite (Rmult la lb)) *)
  apply is_lim_seq_spec.
(* Goal: is_lim_seq' a (Finite (IZR Z0)) *)
  intros eps.
(* Goal: eventually (fun n : nat => Rlt (Rabs (Rminus (a n) (IZR Z0))) (pos eps)) *)
  apply (Cauchy_ex_series (V := R_CompleteNormedModule)) in Hs.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: (Hs eps) => {Hs} N Hs.
(* Goal: eventually (fun n : nat => Rlt (Rabs (Rminus (a n) (IZR Z0))) (pos eps)) *)
  exists (S N) ; case => [ | n] Hn.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply le_Sn_0 in Hn.
(* Goal: Rlt (Rabs (Rminus (a (S n)) (IZR Z0))) (pos eps) *)
  apply le_S_n in Hn.
  replace (a (S n) - 0)
    with (sum_n_m a (S n) (S n)).
(* Goal: @eq R (a (Init.Nat.add n O)) (IZR Z0) *)
(* Goal: forall (k : nat) (_ : lt k n), @eq R (a k) (IZR Z0) *)
  apply Hs ; by intuition.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by rewrite sum_n_n Rminus_0_r.
Qed.

Lemma ex_series_Rabs (a : nat -> R) :
  ex_series (fun n => Rabs (a n)) -> ex_series a.
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => H.
(* Goal: @eq (NormedModule.sort K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a n) (a (S n)))) (@plus (NormedModule.AbelianGroup K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@sum_n (NormedModule.AbelianGroup K V) a n)) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (a (S n)))) *)
(* Goal: @filterlim nat (ModuleSpace.sort (AbsRing.Ring K) (NormedModule.ModuleSpace K V)) (fun n : nat => @scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@sum_n (NormedModule.AbelianGroup K V) a n)) eventually (@locally (NormedModule.UniformSpace K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c l)) *)
  apply: ex_series_Cauchy.
  apply Cauchy_series_Reals.
  apply cauchy_abs.
  apply Cauchy_series_Reals.
(* Goal: @eq (NormedModule.sort K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a n) (a (S n)))) (@plus (NormedModule.AbelianGroup K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@sum_n (NormedModule.AbelianGroup K V) a n)) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (a (S n)))) *)
(* Goal: @filterlim nat (ModuleSpace.sort (AbsRing.Ring K) (NormedModule.ModuleSpace K V)) (fun n : nat => @scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@sum_n (NormedModule.AbelianGroup K V) a n)) eventually (@locally (NormedModule.UniformSpace K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c l)) *)
  by apply: Cauchy_ex_series.
Qed.

Lemma Series_Rabs (a : nat -> R) :
  ex_series (fun n => Rabs (a n)) ->
    Rabs (Series a) <= Series (fun n => Rabs (a n)).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Hra.
(* Goal: False *)
  have Ha := (ex_series_Rabs a Hra).
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: Hra => lra Hra.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: Ha => la Ha.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite /is_series in Hra Ha.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite /Series /=.
  replace (Lim_seq (sum_n a)) with (Finite la).
  replace (Lim_seq (sum_n (fun k : nat => Rabs (a k)))) with (Finite lra).
  simpl.
  apply (is_lim_seq_abs _ la) in Ha.
  change (Rbar_le (Rabs la) lra).
  eapply is_lim_seq_le with (2:=Ha).
  2: apply Hra.
(* Goal: forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
  elim => [ | n IH] /=.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite !sum_O.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Rle_refl.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite !sum_Sn.
  apply Rle_trans with (1 := Rabs_triang _ _).
  apply Rplus_le_compat_r.
(* Goal: @is_series K V (fun k : nat => a (S k)) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O))) *)
  by apply IH.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply sym_eq, is_lim_seq_unique.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply sym_eq, is_lim_seq_unique.
Qed.

(** Comparison *)

Lemma ex_series_le {K : AbsRing} {V : CompleteNormedModule K}
  (a : nat -> V) (b : nat -> R) :
   (forall n : nat, norm (a n) <= b n) ->
   ex_series b -> ex_series a.
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => H Hb.
  apply (Cauchy_ex_series (V := R_CompleteNormedModule)) in Hb.
  apply ex_series_Cauchy.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => e.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case (Hb e) => {Hb} N Hb.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  exists N => n m Hn Hm.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  eapply Rle_lt_trans, (Hb _ _ Hn Hm) => //.
  eapply Rle_trans.
  apply norm_sum_n_m.
  apply Rle_trans with (sum_n_m b n m).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply sum_n_m_le.
  right.
  assert (forall n, 0 <= b n).
    intros k.
    eapply Rle_trans, H.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply norm_ge_0.
  clear -H0.
  apply sym_eq, Rabs_pos_eq.
(* Goal: forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
  elim: n m b H0 => /= [ | n IH] m b Hb.
(* Goal: forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
  elim: m => /= [ | m IH].
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite sum_n_n.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Hb.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite sum_n_Sm.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Rplus_le_le_0_compat.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply le_O_n.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: m => /= [ | m].
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Rle_refl.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite -sum_n_m_S.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  apply IH => k.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Hb.
Qed.

Lemma Series_le (a b : nat -> R) :
  (forall n : nat, 0 <= a n <= b n) ->
   ex_series b -> Series a <= Series b.
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Hn Hb.
(* Goal: False *)
  have Ha := (ex_series_le a b).
(* Goal: Rle (Series a) (Series b) *)
  apply Lim_seq_correct' in Ha.
(* Goal: Rle (Series a) (Series b) *)
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (a n)) (b n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule b *)
  apply Lim_seq_correct' in Hb.
(* Goal: Rle (Series a) (Series b) *)
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (a n)) (b n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule b *)
  move: Ha Hb ; apply is_lim_seq_le.
(* Goal: forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
  elim => [ | n IH] /=.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite !sum_O.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Hn.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite !sum_Sn.
(* Goal: Rle (Rplus (sum_f O (Init.Nat.sub n (S m)) (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l)))) (IZR Z0)) (Rplus (sum_f (S O) (S (Init.Nat.sub n (S m))) (fun k : nat => Rmult (a (Init.Nat.add k (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add k (S m)))))) (sum_f (S (S (Init.Nat.sub n (S m)))) (S (S n)) (fun k : nat => Rmult (a (Init.Nat.add k (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add k (S m))))))) *)
(* Goal: le (S O) (S (S n)) *)
(* Goal: Rle (IZR Z0) (Rmult (a O) (b (S (S (S (Init.Nat.add m n)))))) *)
(* Goal: @eq R (Rplus (sum_f (S O) (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) (Rmult (a O) (b (S (S (S (Init.Nat.add m n))))))) (sum_f O (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
  apply Rplus_le_compat.
(* Goal: @is_series K V (fun k : nat => a (S k)) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O))) *)
  by apply IH.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Hn.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (a n)) (b n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule b *)
  intros n.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  rewrite /norm /= /abs /= Rabs_pos_eq ; by apply Hn.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Hb.
Qed.


(** * Operations *)

(** Additive operators *)

Section Properties2.

Context {K : AbsRing} {V : NormedModule K}.

Lemma is_series_opp (a : nat -> V) (la : V) :
  is_series a la
    -> is_series (fun n => opp (a n)) (opp la).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Ha.
(* Goal: @is_series K V (fun n : nat => @opp (NormedModule.AbelianGroup K V) (a n)) (@opp (NormedModule.AbelianGroup K V) la) *)
   apply filterlim_ext with (fun n => opp (sum_n a n)).
(* Goal: forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
  elim => [ | n IH].
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@opp (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a O)) (@sum_n (NormedModule.AbelianGroup K V) (fun n : nat => @opp (NormedModule.AbelianGroup K V) (a n)) O) *)
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@opp (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a (S n))) (@sum_n (NormedModule.AbelianGroup K V) (fun n : nat => @opp (NormedModule.AbelianGroup K V) (a n)) (S n)) *)
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun n : nat => @opp (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a n)) eventually (@locally (NormedModule.UniformSpace K V) (@opp (NormedModule.AbelianGroup K V) la)) *)
  rewrite !sum_O ; easy.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite !sum_Sn -IH.
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@opp (NormedModule.AbelianGroup K V) (@plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a n) (a (S n)))) (@plus (NormedModule.AbelianGroup K V) (@opp (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a n)) (@opp (NormedModule.AbelianGroup K V) (a (S n)))) *)
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun n : nat => @opp (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a n)) eventually (@locally (NormedModule.UniformSpace K V) (@opp (NormedModule.AbelianGroup K V) la)) *)
  apply opp_plus.
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun n : nat => @opp (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a n)) eventually (@locally (NormedModule.UniformSpace K V) (@opp (NormedModule.AbelianGroup K V) la)) *)
  apply filterlim_comp with (1:=Ha).
(* Goal: @filterlim (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@opp (NormedModule.AbelianGroup K V)) (@locally (NormedModule.UniformSpace K V) la) (@locally (NormedModule.UniformSpace K V) (@opp (NormedModule.AbelianGroup K V) la)) *)
  apply filterlim_opp.
Qed.

Lemma ex_series_opp (a : nat -> V) :
  ex_series a
    -> ex_series (fun n => opp (a n)).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => [la Ha].
(* Goal: @ex_series K V (fun n : nat => @opp (NormedModule.AbelianGroup K V) (a n)) *)
  exists (opp la).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply is_series_opp.
Qed.
Lemma Series_opp (a : nat -> R) :
  Series (fun n => - a n) = - Series a.
Proof.
  rewrite /Series
    (Lim_seq_ext (sum_n (fun k : nat => - a k)) (fun n => - (sum_n (fun k => a k) n))).
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite Lim_seq_opp.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by rewrite Rbar_opp_real.
(* Goal: forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
  elim => [ | n IH].
(* Goal: @eq R (@sum_n R_AbelianGroup (fun n : nat => Rmult c (a n)) O) (Rmult c (@sum_n R_AbelianGroup a O)) *)
(* Goal: @eq R (@sum_n R_AbelianGroup (fun n : nat => Rmult c (a n)) (S n)) (Rmult c (@sum_n R_AbelianGroup a (S n))) *)
  rewrite !sum_O ; ring.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite !sum_Sn IH /plus /=.
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult (Rminus (Series ap) (Series am)) (Rminus (Series bp) (Series bm))) *)
(* Goal: @eq R (Rminus (Series bp) (Series bm)) lb *)
(* Goal: @eq R (Rminus (Series ap) (Series am)) la *)
  ring.
Qed.

Lemma is_series_plus (a b : nat -> V) (la lb : V) :
  is_series a la -> is_series b lb
    -> is_series (fun n => plus (a n)  (b n)) (plus la  lb).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Ha Hb.
(* Goal: @is_series K V (fun n : nat => @plus (NormedModule.AbelianGroup K V) (a n) (b n)) (@plus (NormedModule.AbelianGroup K V) la lb) *)
  apply filterlim_ext with (fun n => plus (sum_n a n) (sum_n b n)).
  elim => [ | n IH]; simpl.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  by rewrite !sum_O.
(* Goal: @eq R (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (Init.Nat.add (S k) O))) (b (Init.Nat.sub (S n) (S k))))) (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (S k))) (b (Init.Nat.sub (S (S n)) (S (S k)))))) *)
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) m) (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) (S m))))) (Rplus (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) m) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p))) (Init.Nat.add (S m) (S (S n))))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
  rewrite !sum_Sn -IH; rewrite <- 2!plus_assoc; apply f_equal.
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a (S n)) (@plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) b n) (b (S n)))) (@plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) b n) (@plus (NormedModule.AbelianGroup K V) (a (S n)) (b (S n)))) *)
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun n : nat => @plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a n) (@sum_n (NormedModule.AbelianGroup K V) b n)) eventually (@locally (NormedModule.UniformSpace K V) (@plus (NormedModule.AbelianGroup K V) la lb)) *)
  rewrite 2!plus_assoc; apply f_equal2; try easy.
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a (S n)) (@sum_n (NormedModule.AbelianGroup K V) b n)) (@plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) b n) (a (S n))) *)
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun n : nat => @plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a n) (@sum_n (NormedModule.AbelianGroup K V) b n)) eventually (@locally (NormedModule.UniformSpace K V) (@plus (NormedModule.AbelianGroup K V) la lb)) *)
  apply plus_comm.
(* Goal: @filterlim nat (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (fun v : nat => @plus (NormedModule.AbelianGroup K V) (a O) (@sum_n (NormedModule.AbelianGroup K V) (fun k : nat => a (S k)) (Init.Nat.pred v))) eventually (@locally (NormedModule.UniformSpace K V) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O))))) *)
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) (a O) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O)))) l *)
  now apply filterlim_comp_2 with (3 := filterlim_plus _ _).
Qed.
Lemma ex_series_plus (a b : nat -> V) :
  ex_series a -> ex_series b
    -> ex_series (fun n => plus (a n) (b n)).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => [la Ha] [lb Hb].
(* Goal: @ex_series K V (fun n : nat => @plus (NormedModule.AbelianGroup K V) (a n) (b n)) *)
  exists (plus la lb).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply is_series_plus.
Qed.

Lemma is_series_minus (a b : nat -> V) (la lb : V) :
  is_series a la -> is_series b lb
    -> is_series (fun n => plus (a n) (opp (b n))) (plus la (opp lb)).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Ha Hb.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  apply is_series_plus => //.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  apply is_series_opp => //.
Qed.
Lemma ex_series_minus (a b : nat -> V) :
  ex_series a -> ex_series b
    -> ex_series (fun n => plus (a n) (opp (b n))).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Ha Hb.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  apply ex_series_plus => //.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  apply ex_series_opp => //.
Qed.

End Properties2.

Lemma Series_plus (a b : nat -> R) :
  ex_series a -> ex_series b
    -> Series (fun n => a n + b n) = Series a + Series b.
Proof.
(* Goal: forall (_ : @ex_series R_AbsRing R_NormedModule a) (_ : @ex_series R_AbsRing R_NormedModule b), @eq R (Series (fun n : nat => Rminus (a n) (b n))) (Rminus (Series a) (Series b)) *)
  intros Ha Hb.
(* Goal: @eq R (Series (fun n : nat => Rplus (a n) (b n))) (Rplus (Series a) (Series b)) *)
  replace (Series a + Series b) with (real (Series a + Series b)) by auto.
(* Goal: @eq R (Series (fun n : nat => Rplus (a n) (b n))) (real (Finite (Rplus (Series a) (Series b)))) *)
  apply (f_equal real), is_lim_seq_unique.
  apply: is_series_plus ;
(* Goal: @is_series R_AbsRing R_NormedModule (fun k : nat => a (Init.Nat.add n k)) (Series (fun k : nat => a (Init.Nat.add n k))) *)
  by apply Series_correct.
Qed.

Lemma Series_minus (a b : nat -> R) :
  ex_series a -> ex_series b
    -> Series (fun n => a n - b n) = Series a - Series b.
Proof.
(* Goal: forall (_ : @ex_series R_AbsRing R_NormedModule a) (_ : @ex_series R_AbsRing R_NormedModule b), @eq R (Series (fun n : nat => Rminus (a n) (b n))) (Rminus (Series a) (Series b)) *)
  intros Ha Hb.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  rewrite Series_plus => //.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  rewrite Series_opp => //.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Ropp (b n)) *)
  apply ex_series_opp in Hb.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Ropp (b n)) *)
  now simpl in Hb.
Qed.

(** Multiplication by a scalar *)

Section Properties3.

Context {K : AbsRing} {V : NormedModule K}.

Lemma is_series_scal (c : K) (a : nat -> V) (l : V) :
  is_series a l -> is_series (fun n => scal c (a n)) (scal c l).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Ha.
(* Goal: @is_series K V (fun n : nat => @scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (a n)) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c l) *)
  apply filterlim_ext with (fun n => scal c (sum_n a n)).
  elim => [ | n IH]; simpl.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  by rewrite !sum_O.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite !sum_Sn -IH.
(* Goal: @eq (NormedModule.sort K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@plus (NormedModule.AbelianGroup K V) (@sum_n (NormedModule.AbelianGroup K V) a n) (a (S n)))) (@plus (NormedModule.AbelianGroup K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@sum_n (NormedModule.AbelianGroup K V) a n)) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (a (S n)))) *)
(* Goal: @filterlim nat (ModuleSpace.sort (AbsRing.Ring K) (NormedModule.ModuleSpace K V)) (fun n : nat => @scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@sum_n (NormedModule.AbelianGroup K V) a n)) eventually (@locally (NormedModule.UniformSpace K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c l)) *)
  apply: scal_distr_l.
(* Goal: @filterlim nat (ModuleSpace.sort (AbsRing.Ring K) (NormedModule.ModuleSpace K V)) (fun n : nat => @scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@sum_n (NormedModule.AbelianGroup K V) a n)) eventually (@locally (NormedModule.UniformSpace K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c l)) *)
  now apply filterlim_comp with (2 := filterlim_scal_r _ _).
Qed.
Lemma is_series_scal_l : forall (c : K) (a : nat -> V) (l : V),
  is_series a l -> is_series (fun n => scal c (a n)) (scal c l).
(* Goal: forall (c : AbsRing.sort K) (a : forall _ : nat, NormedModule.sort K V) (l : NormedModule.sort K V) (_ : @is_series K V a l), @is_series K V (fun n : nat => @scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (a n)) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c l) *)
exact is_series_scal.
Qed.

Lemma ex_series_scal (c : K) (a : nat -> V) :
  ex_series a -> ex_series (fun n => scal c (a n)).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => [l Ha].
(* Goal: @ex_series K V (fun n : nat => @scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (a n)) *)
  exists (scal c l).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply: is_series_scal_l.
Qed.

Lemma ex_series_scal_l : forall (c : K) (a : nat -> V),
  ex_series a -> ex_series (fun n => scal c (a n)).
(* Goal: forall (c : AbsRing.sort K) (a : forall _ : nat, NormedModule.sort K V) (_ : @ex_series K V a), @ex_series K V (fun n : nat => @scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (a n)) *)
exact ex_series_scal.
Qed.

End Properties3.

Lemma Series_scal_l (c : R) (a : nat -> R) :
  Series (fun n => c * a n) = c * Series a.
Proof.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite /Series.
(* Goal: False *)
  have H0 : (forall x, c * Rbar.real x = Rbar.real (Rbar.Rbar_mult (Rbar.Finite c) x)).
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: (Req_dec c 0) => [-> | Hk].
(* Goal: forall x : Rbar, @eq R (Rmult c (real x)) (real (Rbar_mult (Finite c) x)) *)
(* Goal: @eq R (real (Lim_seq (@sum_n R_AbelianGroup (fun n : nat => Rmult c (a n))))) (Rmult c (real (Lim_seq (@sum_n R_AbelianGroup a)))) *)
  case => [x | | ] //= ; rewrite Rmult_0_l.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: Rle_dec (Rle_refl 0) => //= H0 _.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: Rle_lt_or_eq_dec (Rlt_irrefl 0) => //= _ _.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: Rle_dec (Rle_refl 0) => //= H0 _.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: Rle_lt_or_eq_dec (Rlt_irrefl 0) => //= _ _.
(* Goal: forall x : Rbar, @eq R (Rmult c (real x)) (real (Rbar_mult (Finite c) x)) *)
(* Goal: @eq R (real (Lim_seq (@sum_n R_AbelianGroup (fun n : nat => Rmult c (a n))))) (Rmult c (real (Lim_seq (@sum_n R_AbelianGroup a)))) *)
  case => [x | | ] //= ; rewrite Rmult_0_r.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: Rle_dec => //= H0.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: Rle_lt_or_eq_dec => //=.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: Rle_dec => //= H0.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: Rle_lt_or_eq_dec => //=.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite H0 -(Lim_seq_scal_l _ c).
(* Goal: @eq R (real (Lim_seq (@sum_n R_AbelianGroup (fun n : nat => Rmult c (a n))))) (real (Lim_seq (fun n : nat => Rmult c (@sum_n R_AbelianGroup a n)))) *)
  apply f_equal, Lim_seq_ext.
(* Goal: forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
  elim => [ | n IH].
(* Goal: @eq R (@sum_n R_AbelianGroup (fun n : nat => Rmult c (a n)) O) (Rmult c (@sum_n R_AbelianGroup a O)) *)
(* Goal: @eq R (@sum_n R_AbelianGroup (fun n : nat => Rmult c (a n)) (S n)) (Rmult c (@sum_n R_AbelianGroup a (S n))) *)
  rewrite !sum_O ; ring.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite !sum_Sn IH /plus /=.
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult (Rminus (Series ap) (Series am)) (Rminus (Series bp) (Series bm))) *)
(* Goal: @eq R (Rminus (Series bp) (Series bm)) lb *)
(* Goal: @eq R (Rminus (Series ap) (Series am)) la *)
  ring.
Qed.

Lemma is_series_scal_r (c : R) (a : nat -> R) (l : R) :
  is_series  a l -> is_series  (fun n => (a n) * c) (l * c).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Ha.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite Rmult_comm.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => Rmult (a n) c) (Rmult c l) *)
  apply is_series_ext with (fun n : nat => c * a n).
(* Goal: forall n : nat, @eq R (Rmult (a n) c) (Rmult c (a n)) *)
  move => n ; apply Rmult_comm.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => Rmult c (a n)) (Rmult c l) *)
  apply (is_series_scal_l _ _ _ Ha).
Qed.
Lemma ex_series_scal_r (c : R) (a : nat -> R) :
  ex_series  a -> ex_series  (fun n => a n * c).
Proof.
(* Goal: forall _ : @ex_series R_AbsRing R_NormedModule a, @ex_series R_AbsRing R_NormedModule (fun n : nat => Rmult (a n) c) *)
  intros [l Ha].
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rmult (a n) c) *)
  exists (l * c).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply is_series_scal_r.
Qed.

Lemma Series_scal_r (c : R) (a : nat -> R) :
  Series (fun n => a n * c) = Series a * c.
Proof.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite Rmult_comm -Series_scal_l.
(* Goal: @eq R (Series (fun n : nat => Rmult (a n) c)) (Series (fun n : nat => Rmult c (a n))) *)
  apply Series_ext.
(* Goal: forall n : nat, @eq R (Rmult (a n) c) (Rmult c (a n)) *)
  move => n ; apply Rmult_comm.
Qed.

Lemma is_series_mult_pos (a b : nat -> R) (la lb : R) :
  is_series  a la -> is_series  b lb ->
  (forall n, 0 <= a n) -> (forall n, 0 <= b n)
  -> is_series  (fun n => sum_f_R0 (fun k => a k * b (n - k)%nat) n) (la * lb).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Hla Hlb Ha Hb.

  have H0 : forall n,
    sum_f_R0 (fun k : nat => sum_f_R0 (fun p : nat => a p * b (k - p)%nat) k) n
      <= sum_f_R0 a n * sum_f_R0 b n.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    case => [ | n].
(* Goal: Rle (sum_f_R0 (fun k : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub k p))) k) O) (Rmult (sum_f_R0 a O) (sum_f_R0 b O)) *)
(* Goal: Rle (sum_f_R0 (fun k : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub k p))) k) (S n)) (Rmult (sum_f_R0 a (S n)) (sum_f_R0 b (S n))) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    simpl ; apply Rle_refl.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite (cauchy_finite a b (S n) (lt_O_Sn n)).
(* Goal: Rle (sum_f O n (fun l : nat => Rmult (a (S (Init.Nat.add l O))) (b (Init.Nat.sub (S n) l)))) (Rplus (Rplus (sum_f O n (fun l0 : nat => Rmult (a (S (Init.Nat.add l0 O))) (b (Init.Nat.sub (S n) l0)))) (Rmult (a (S (S n))) (b (Init.Nat.sub (S (S n)) (S (S n)))))) (Rmult (a O) (b (S (S n))))) *)
(* Goal: Rle (Rplus (Rplus (sum_f O n (fun l0 : nat => Rmult (a (S (Init.Nat.add l0 O))) (b (Init.Nat.sub (S n) l0)))) (Rmult (a (S (S n))) (b (Init.Nat.sub (S (S n)) (S (S n)))))) (Rmult (a O) (b (S (S n))))) (Rplus (Rplus (sum_f O n (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k))))) (Rmult (a (S (S n))) (b (Init.Nat.sub (S (S n)) (S (S n)))))) (Rmult (a O) (b (S (S n))))) *)
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) m) (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) (S m))))) (Rplus (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) m) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p))) (Init.Nat.add (S m) (S (S n))))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply Rminus_le_0 ; ring_simplify.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    apply cond_pos_sum => m.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    apply cond_pos_sum => k.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rmult_le_pos.
  have H1 : forall n, sum_f_R0 a n * sum_f_R0 b n
    <= sum_f_R0 (fun k : nat => sum_f_R0 (fun p : nat => a p * b (k - p)%nat) k) ((2*n)%nat).
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    case => [ /= | n].
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rle_refl.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite (cauchy_finite a b (S n) (lt_O_Sn n)).
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub k p))) k) (S n)) (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) (Init.Nat.pred (S n)))) (sum_f_R0 (fun k : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub k p))) k) (Init.Nat.mul (S (S O)) (S n))) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    rewrite Rplus_comm ; apply Rle_minus_r.
(* Goal: Rle (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) (Init.Nat.pred (S n))) (Rminus (sum_f_R0 (fun k : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub k p))) k) (Init.Nat.mul (S (S O)) (S n))) (sum_f_R0 (fun k : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub k p))) k) (S n))) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    replace (pred (S n)) with n by auto.
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult (Rminus (Series ap) (Series am)) (Rminus (Series bp) (Series bm))) *)
(* Goal: @eq R (Rminus (Series bp) (Series bm)) lb *)
(* Goal: @eq R (Rminus (Series ap) (Series am)) la *)
    replace (2 * S n)%nat with (S n + S n)%nat by ring.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite -sum_f_rw.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite /sum_f.
(* Goal: Rle (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) n) (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n)))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    replace (S n + S n - S (S n))%nat with n.
(* Goal: Rle (IZR Z0) (sum_f_R0 (fun x : nat => Rmult (a (Init.Nat.add (Init.Nat.add x (S (S (Init.Nat.sub n (S m))))) (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add (Init.Nat.add x (S (S (Init.Nat.sub n (S m))))) (S m))))) (Init.Nat.sub (S (S n)) (S (S (Init.Nat.sub n (S m)))))) *)
(* Goal: le (S O) (S (S n)) *)
(* Goal: Rle (IZR Z0) (Rmult (a O) (b (S (S (S (Init.Nat.add m n)))))) *)
(* Goal: @eq R (Rplus (sum_f (S O) (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) (Rmult (a O) (b (S (S (S (Init.Nat.add m n))))))) (sum_f O (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    elim: {1 5 8}n (le_refl n) => [ | m IH] Hm ; rewrite /sum_f_R0 -/sum_f_R0.
(* Goal: Rle (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l O))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) O))) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add O (S (S n))) p))) (Init.Nat.add O (S (S n)))) *)
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) m) (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) (S m))))) (Rplus (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) m) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p))) (Init.Nat.add (S m) (S (S n))))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    rewrite -minus_n_O plus_0_l ; simpl pred.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite -?sum_f_rw_0.
    replace (sum_f 0 (S (S n)) (fun p : nat => a p * b (S (S n) - p)%nat))
      with ((sum_f 0 (S (S n)) (fun p : nat => a p * b (S (S n) - p)%nat) -
        (fun p : nat => a p * b (S (S n) - p)%nat) 0%nat)
        + a O * b (S (S n))) by (rewrite -minus_n_O ; ring).
(* Goal: Rle (sum_f O n (fun l : nat => Rmult (a (S (Init.Nat.add l O))) (b (Init.Nat.sub (S n) l)))) (Rplus (sum_f O (S n) (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k))))) (Rmult (a O) (b (S (S n))))) *)
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) m) (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) (S m))))) (Rplus (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) m) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p))) (Init.Nat.add (S m) (S (S n))))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    rewrite -(sum_f_Sn_m _ O (S (S n))) ; [ | by apply lt_O_Sn].
(* Goal: Rle (sum_f O n (fun l : nat => Rmult (a (S (Init.Nat.add l O))) (b (Init.Nat.sub (S n) l)))) (Rplus (sum_f O (S n) (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k))))) (Rmult (a O) (b (S (S n))))) *)
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) m) (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) (S m))))) (Rplus (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) m) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p))) (Init.Nat.add (S m) (S (S n))))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    rewrite sum_f_u_Sk ; [ | by apply le_O_n].
(* Goal: Rle (sum_f O n (fun l : nat => Rmult (a (S (Init.Nat.add l O))) (b (Init.Nat.sub (S n) l)))) (Rplus (sum_f O (S n) (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k))))) (Rmult (a O) (b (S (S n))))) *)
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) m) (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) (S m))))) (Rplus (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) m) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p))) (Init.Nat.add (S m) (S (S n))))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    rewrite sum_f_n_Sm ; [ | by apply le_O_n].
    apply Rle_trans with (sum_f 0 n (fun l0 : nat => a (S (l0 + 0)) * b (S n - l0)%nat) +
      a (S (S n)) * b (S (S n) - S (S n))%nat + a 0%nat * b (S (S n))).
(* Goal: Rle (sum_f O n (fun l : nat => Rmult (a (S (Init.Nat.add l O))) (b (Init.Nat.sub (S n) l)))) (Rplus (Rplus (sum_f O n (fun l0 : nat => Rmult (a (S (Init.Nat.add l0 O))) (b (Init.Nat.sub (S n) l0)))) (Rmult (a (S (S n))) (b (Init.Nat.sub (S (S n)) (S (S n)))))) (Rmult (a O) (b (S (S n))))) *)
(* Goal: Rle (Rplus (Rplus (sum_f O n (fun l0 : nat => Rmult (a (S (Init.Nat.add l0 O))) (b (Init.Nat.sub (S n) l0)))) (Rmult (a (S (S n))) (b (Init.Nat.sub (S (S n)) (S (S n)))))) (Rmult (a O) (b (S (S n))))) (Rplus (Rplus (sum_f O n (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k))))) (Rmult (a (S (S n))) (b (Init.Nat.sub (S (S n)) (S (S n)))))) (Rmult (a O) (b (S (S n))))) *)
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) m) (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) (S m))))) (Rplus (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) m) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p))) (Init.Nat.add (S m) (S (S n))))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
      apply Rminus_le_0 ; ring_simplify.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
      apply Rplus_le_le_0_compat ; by apply Rmult_le_pos.
      repeat apply Rplus_le_compat_r.
(* Goal: Rle (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.sub n (S m))) (sum_f_R0 (fun k : nat => Rmult (a (Init.Nat.add (S k) (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add (S k) (S m))))) (Init.Nat.sub n (S m))) *)
(* Goal: le O (Init.Nat.sub n (S m)) *)
(* Goal: Rle (IZR Z0) (sum_f (S (S (Init.Nat.sub n (S m)))) (S (S n)) (fun k : nat => Rmult (a (Init.Nat.add k (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add k (S m)))))) *)
(* Goal: le (S O) (S (S n)) *)
(* Goal: Rle (IZR Z0) (Rmult (a O) (b (S (S (S (Init.Nat.add m n)))))) *)
(* Goal: @eq R (Rplus (sum_f (S O) (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) (Rmult (a O) (b (S (S (S (Init.Nat.add m n))))))) (sum_f O (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
      apply Req_le.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
      rewrite ?sum_f_rw_0.
      elim: {1 4 6}n (le_refl n) => [ | k IH] Hk // ;
      rewrite /sum_f_R0 -/sum_f_R0.
(* Goal: @eq R (a (Init.Nat.add n O)) (IZR Z0) *)
(* Goal: forall (k : nat) (_ : lt k n), @eq R (a k) (IZR Z0) *)
      rewrite IH ; try by intuition.
(* Goal: @eq R (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (Init.Nat.add (S k) O))) (b (Init.Nat.sub (S n) (S k))))) (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (S k))) (b (Init.Nat.sub (S (S n)) (S (S k)))))) *)
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) m) (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) (S m))))) (Rplus (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) m) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p))) (Init.Nat.add (S m) (S (S n))))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
      apply f_equal.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
      by rewrite plus_0_r /=.
(* Goal: Rle (Rplus (sum_f O (Init.Nat.sub n (S m)) (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l)))) (IZR Z0)) (Rplus (sum_f (S O) (S (Init.Nat.sub n (S m))) (fun k : nat => Rmult (a (Init.Nat.add k (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add k (S m)))))) (sum_f (S (S (Init.Nat.sub n (S m)))) (S (S n)) (fun k : nat => Rmult (a (Init.Nat.add k (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add k (S m))))))) *)
(* Goal: le (S O) (S (S n)) *)
(* Goal: Rle (IZR Z0) (Rmult (a O) (b (S (S (S (Init.Nat.add m n)))))) *)
(* Goal: @eq R (Rplus (sum_f (S O) (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) (Rmult (a O) (b (S (S (S (Init.Nat.add m n))))))) (sum_f O (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply Rplus_le_compat.
(* Goal: @eq R (a (Init.Nat.add n O)) (IZR Z0) *)
(* Goal: forall (k : nat) (_ : lt k n), @eq R (a k) (IZR Z0) *)
    apply IH ; intuition.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite -?sum_f_rw_0.
(* Goal: @eq R (a (Init.Nat.add n O)) (IZR Z0) *)
(* Goal: forall (k : nat) (_ : lt k n), @eq R (a k) (IZR Z0) *)
    rewrite MyNat.sub_succ_l ; try by intuition.
(* Goal: Rle (sum_f O (Init.Nat.pred (S (Init.Nat.sub n (S m)))) (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l)))) (sum_f O (Init.Nat.add (S m) (S (S n))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p)))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    replace (pred (S (n - S m))) with (n - S m)%nat by auto.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite plus_Sn_m -?plus_n_Sm.
    replace (sum_f 0 (S (S (S (m + n))))
      (fun p : nat => a p * b (S (S (S (m + n))) - p)%nat))
      with (sum_f 1 (S (S (S (m + n))))
      (fun p : nat => a p * b (S (S (S (m + n))) - p)%nat) + a O * b (S (S (S (m + n))))).
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite -(Rplus_0_r (sum_f O _ _)).
(* Goal: Rle (Rplus (sum_f O (Init.Nat.sub n (S m)) (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l)))) (IZR Z0)) (Rplus (sum_f (S O) (S (Init.Nat.sub n (S m))) (fun k : nat => Rmult (a (Init.Nat.add k (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add k (S m)))))) (sum_f (S (S (Init.Nat.sub n (S m)))) (S (S n)) (fun k : nat => Rmult (a (Init.Nat.add k (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add k (S m))))))) *)
(* Goal: le (S O) (S (S n)) *)
(* Goal: Rle (IZR Z0) (Rmult (a O) (b (S (S (S (Init.Nat.add m n)))))) *)
(* Goal: @eq R (Rplus (sum_f (S O) (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) (Rmult (a O) (b (S (S (S (Init.Nat.add m n))))))) (sum_f O (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply Rplus_le_compat.
(* Goal: @eq R (a (Init.Nat.add n O)) (IZR Z0) *)
(* Goal: forall (k : nat) (_ : lt k n), @eq R (a k) (IZR Z0) *)
    rewrite (sum_f_chasles _ O (S m) (S (S (S (m + n))))) ; try by intuition.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite -(Rplus_0_l (sum_f O _ _)).
(* Goal: Rle (Rplus (sum_f O (Init.Nat.sub n (S m)) (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l)))) (IZR Z0)) (Rplus (sum_f (S O) (S (Init.Nat.sub n (S m))) (fun k : nat => Rmult (a (Init.Nat.add k (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add k (S m)))))) (sum_f (S (S (Init.Nat.sub n (S m)))) (S (S n)) (fun k : nat => Rmult (a (Init.Nat.add k (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add k (S m))))))) *)
(* Goal: le (S O) (S (S n)) *)
(* Goal: Rle (IZR Z0) (Rmult (a O) (b (S (S (S (Init.Nat.add m n)))))) *)
(* Goal: @eq R (Rplus (sum_f (S O) (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) (Rmult (a O) (b (S (S (S (Init.Nat.add m n))))))) (sum_f O (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply Rplus_le_compat.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite /sum_f.
(* Goal: Rle (IZR Z0) (sum_f_R0 (fun x : nat => Rmult (a (Init.Nat.add (Init.Nat.add x (S (S (Init.Nat.sub n (S m))))) (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add (Init.Nat.add x (S (S (Init.Nat.sub n (S m))))) (S m))))) (Init.Nat.sub (S (S n)) (S (S (Init.Nat.sub n (S m)))))) *)
(* Goal: le (S O) (S (S n)) *)
(* Goal: Rle (IZR Z0) (Rmult (a O) (b (S (S (S (Init.Nat.add m n)))))) *)
(* Goal: @eq R (Rplus (sum_f (S O) (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) (Rmult (a O) (b (S (S (S (Init.Nat.add m n))))))) (sum_f O (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    elim: (S m - 1)%nat => {IH} [ | k IH] ; rewrite /sum_f_R0 -/sum_f_R0 //.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rmult_le_pos.
(* Goal: Rle (IZR Z0) (Rplus (sum_f_R0 (fun x : nat => Rmult (a (Init.Nat.add x (S O))) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) (Init.Nat.add x (S O))))) k) (Rmult (a (Init.Nat.add (S k) (S O))) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) (Init.Nat.add (S k) (S O)))))) *)
(* Goal: Rle (sum_f O (Init.Nat.sub n (S m)) (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l)))) (sum_f (S (S m)) (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) *)
(* Goal: Rle (IZR Z0) (Rmult (a O) (b (S (S (S (Init.Nat.add m n)))))) *)
(* Goal: @eq R (Rplus (sum_f (S O) (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) (Rmult (a O) (b (S (S (S (Init.Nat.add m n))))))) (sum_f O (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply Rplus_le_le_0_compat.
(* Goal: @is_series K V (fun k : nat => a (S k)) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O))) *)
    by apply IH.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rmult_le_pos.
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult (Rminus (Series ap) (Series am)) (Rminus (Series bp) (Series bm))) *)
(* Goal: @eq R (Rminus (Series bp) (Series bm)) lb *)
(* Goal: @eq R (Rminus (Series ap) (Series am)) la *)
    replace (S (S m)) with (1 + S m)%nat by ring.
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult (Rminus (Series ap) (Series am)) (Rminus (Series bp) (Series bm))) *)
(* Goal: @eq R (Rminus (Series bp) (Series bm)) lb *)
(* Goal: @eq R (Rminus (Series ap) (Series am)) la *)
    replace (S (S (S (m + n)))) with (S (S n) + S m )%nat by ring.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite sum_f_u_add.
(* Goal: @eq R (a (Init.Nat.add n O)) (IZR Z0) *)
(* Goal: forall (k : nat) (_ : lt k n), @eq R (a k) (IZR Z0) *)
    rewrite (sum_f_chasles _ O (S (n - S m)) (S (S n))) ; try by intuition.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite -(Rplus_0_r (sum_f O _ _)).
(* Goal: Rle (Rplus (sum_f O (Init.Nat.sub n (S m)) (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l)))) (IZR Z0)) (Rplus (sum_f (S O) (S (Init.Nat.sub n (S m))) (fun k : nat => Rmult (a (Init.Nat.add k (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add k (S m)))))) (sum_f (S (S (Init.Nat.sub n (S m)))) (S (S n)) (fun k : nat => Rmult (a (Init.Nat.add k (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add k (S m))))))) *)
(* Goal: le (S O) (S (S n)) *)
(* Goal: Rle (IZR Z0) (Rmult (a O) (b (S (S (S (Init.Nat.add m n)))))) *)
(* Goal: @eq R (Rplus (sum_f (S O) (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) (Rmult (a O) (b (S (S (S (Init.Nat.add m n))))))) (sum_f O (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply Rplus_le_compat.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite sum_f_u_Sk.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite ?sum_f_rw_0.
(* Goal: Rle (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.sub n (S m))) (sum_f_R0 (fun k : nat => Rmult (a (Init.Nat.add (S k) (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add (S k) (S m))))) (Init.Nat.sub n (S m))) *)
(* Goal: le O (Init.Nat.sub n (S m)) *)
(* Goal: Rle (IZR Z0) (sum_f (S (S (Init.Nat.sub n (S m)))) (S (S n)) (fun k : nat => Rmult (a (Init.Nat.add k (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add k (S m)))))) *)
(* Goal: le (S O) (S (S n)) *)
(* Goal: Rle (IZR Z0) (Rmult (a O) (b (S (S (S (Init.Nat.add m n)))))) *)
(* Goal: @eq R (Rplus (sum_f (S O) (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) (Rmult (a O) (b (S (S (S (Init.Nat.add m n))))))) (sum_f O (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply Req_le.
(* Goal: Rle (IZR Z0) (sum_f_R0 (fun x : nat => Rmult (a (Init.Nat.add (Init.Nat.add x (S (S (Init.Nat.sub n (S m))))) (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add (Init.Nat.add x (S (S (Init.Nat.sub n (S m))))) (S m))))) (Init.Nat.sub (S (S n)) (S (S (Init.Nat.sub n (S m)))))) *)
(* Goal: le (S O) (S (S n)) *)
(* Goal: Rle (IZR Z0) (Rmult (a O) (b (S (S (S (Init.Nat.add m n)))))) *)
(* Goal: @eq R (Rplus (sum_f (S O) (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) (Rmult (a O) (b (S (S (S (Init.Nat.add m n))))))) (sum_f O (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    elim: (n - S m)%nat => {IH} [ | k IH] ; rewrite /sum_f_R0 -/sum_f_R0 //.
(* Goal: @eq R (a (Init.Nat.add n O)) (IZR Z0) *)
(* Goal: forall (k : nat) (_ : lt k n), @eq R (a k) (IZR Z0) *)
    apply f_equal2 ; apply f_equal ; intuition.
(* Goal: @eq R (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (Init.Nat.add (S k) O))) (b (Init.Nat.sub (S n) (S k))))) (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (S k))) (b (Init.Nat.sub (S (S n)) (S (S k)))))) *)
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) m) (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) (S m))))) (Rplus (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) m) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p))) (Init.Nat.add (S m) (S (S n))))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    rewrite IH ; apply f_equal, f_equal2 ; apply f_equal.
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult (Rminus (Series ap) (Series am)) (Rminus (Series bp) (Series bm))) *)
(* Goal: @eq R (Rminus (Series bp) (Series bm)) lb *)
(* Goal: @eq R (Rminus (Series ap) (Series am)) la *)
    ring.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite ?(Coq.Arith.Plus.plus_comm _ (S m)) -minus_plus_simpl_l_reverse //=.
(* Goal: le O (Init.Nat.sub n (S m)) *)
(* Goal: Rle (IZR Z0) (sum_f (S (S (Init.Nat.sub n (S m)))) (S (S n)) (fun k : nat => Rmult (a (Init.Nat.add k (S m))) (b (Init.Nat.sub (Init.Nat.add (S (S n)) (S m)) (Init.Nat.add k (S m)))))) *)
(* Goal: le (S O) (S (S n)) *)
(* Goal: Rle (IZR Z0) (Rmult (a O) (b (S (S (S (Init.Nat.add m n)))))) *)
(* Goal: @eq R (Rplus (sum_f (S O) (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) (Rmult (a O) (b (S (S (S (Init.Nat.add m n))))))) (sum_f O (S (S (S (Init.Nat.add m n)))) (fun p : nat => Rmult (a p) (b (Init.Nat.sub (S (S (S (Init.Nat.add m n)))) p)))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply le_O_n.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite /sum_f.
    elim: (S (S n) - S (S (n - S m)))%nat => {IH} [ | k IH] ;
    rewrite /sum_f_R0 -/sum_f_R0 //.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rmult_le_pos.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    apply Rplus_le_le_0_compat => // ; by apply Rmult_le_pos.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply le_n_S, le_O_n.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rmult_le_pos.
(* Goal: @eq R (a (Init.Nat.add n O)) (IZR Z0) *)
(* Goal: forall (k : nat) (_ : lt k n), @eq R (a k) (IZR Z0) *)
    rewrite sum_f_Sn_m -?minus_n_O ; try by intuition.
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult (Rminus (Series ap) (Series am)) (Rminus (Series bp) (Series bm))) *)
(* Goal: @eq R (Rminus (Series bp) (Series bm)) lb *)
(* Goal: @eq R (Rminus (Series ap) (Series am)) la *)
    ring.
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    replace (S (S n)) with (S n + 1)%nat.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite -minus_plus_simpl_l_reverse.
(* Goal: @eq nat n (Init.Nat.sub (S n) (S O)) *)
(* Goal: @eq nat (Init.Nat.add (S n) (S O)) (S (S n)) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    simpl; apply minus_n_O.
(* Goal: @eq nat (Init.Nat.add (S n) (S O)) (S (S n)) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    now rewrite Coq.Arith.Plus.plus_comm.
(* Goal: forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
    elim: n => [ | n IH] //.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite -plus_n_Sm plus_Sn_m.
(* Goal: @eq R (a (Init.Nat.add n O)) (IZR Z0) *)
(* Goal: forall (k : nat) (_ : lt k n), @eq R (a k) (IZR Z0) *)
    apply lt_n_S ; intuition.
    have H2 : forall n, sum_f_R0 a (Div2.div2 n)%nat * sum_f_R0 b (Div2.div2 n)%nat <=
      sum_f_R0
      (fun k : nat => sum_f_R0 (fun p : nat => a p * b (k - p)%nat) k)
      n.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
      move => n.
(* Goal: Rle (Rmult (sum_f_R0 a (Nat.div2 n)) (sum_f_R0 b (Nat.div2 n))) (sum_f_R0 (fun k : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub k p))) k) n) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
      case: (even_odd_cor n) => k ; case => -> {n}.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
      rewrite div2_double.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
      by apply H1.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
      rewrite div2_S_double.
(* Goal: Rle (Rmult (sum_f_R0 a k) (sum_f_R0 b k)) (sum_f_R0 (fun k : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub k p))) k) (S (Init.Nat.mul (S (S O)) k))) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
      apply Rle_trans with (1 := H1 _).
(* Goal: @eq R (a (Init.Nat.add n O)) (IZR Z0) *)
(* Goal: forall (k : nat) (_ : lt k n), @eq R (a k) (IZR Z0) *)
      apply Rminus_le_0 ; rewrite -sum_f_rw ; try by intuition.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
      rewrite /sum_f minus_diag /sum_f_R0 -/sum_f_R0.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
      apply cond_pos_sum => l ; by apply Rmult_le_pos.

(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    change (is_lim_seq (sum_n (fun n : nat => sum_f_R0 (fun k : nat => a k * b (n - k)%nat) n)) (Finite (la * lb))).
    apply is_lim_seq_le_le with (u := fun n => sum_f_R0 a (Div2.div2 n) * sum_f_R0 b (Div2.div2 n))
    (w := fun n => sum_f_R0 a n * sum_f_R0 b n).
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    intros n; rewrite sum_n_Reals.
    by split.
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a (Nat.div2 n)) (sum_f_R0 b (Nat.div2 n))) (Finite (Rmult la lb)) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Finite (Rmult la lb)) *)
    replace (Finite (la * lb)) with (Rbar_mult la lb) by auto.
    suff H : is_lim_seq
      (fun n : nat => sum_f_R0 a n * sum_f_R0 b n)
      (Rbar_mult la lb).
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle (Rabs (Rdiv (a (S n)) (a n))) (Rdiv (Rplus k (IZR (Zpos xH))) (IZR (Zpos (xO xH))))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle (Rabs (Rdiv (a (S n)) (a n))) (Rdiv (Rplus k (IZR (Zpos xH))) (IZR (Zpos (xO xH))))), @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (a n)) *)
    apply is_lim_seq_spec in H.
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a (Nat.div2 n)) (sum_f_R0 b (Nat.div2 n))) (Rbar_mult (Finite la) (Finite lb)) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Rbar_mult (Finite la) (Finite lb)) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Finite (Rmult la lb)) *)
    apply is_lim_seq_spec.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    move => eps.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    case: (H eps) => {H} N H.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    exists (S (2 * N))%nat => n Hn.
(* Goal: Rlt (Rabs (Rminus (Rmult (sum_f_R0 a (Nat.div2 n)) (sum_f_R0 b (Nat.div2 n))) (Rmult la lb))) (pos eps) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Rbar_mult (Finite la) (Finite lb)) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Finite (Rmult la lb)) *)
    apply H.
(* Goal: le N (Nat.div2 n) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Rbar_mult (Finite la) (Finite lb)) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Finite (Rmult la lb)) *)
    apply le_double.
(* Goal: le (Init.Nat.mul (S (S O)) N) (Init.Nat.mul (S (S O)) (Nat.div2 n)) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Rbar_mult (Finite la) (Finite lb)) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Finite (Rmult la lb)) *)
    apply le_S_n.
(* Goal: le (S (Init.Nat.mul (S (S O)) N)) (S (Init.Nat.mul (S (S O)) (Nat.div2 n))) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Rbar_mult (Finite la) (Finite lb)) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Finite (Rmult la lb)) *)
    apply le_trans with (1 := Hn).
(* Goal: le n (S (Init.Nat.mul (S (S O)) (Nat.div2 n))) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Rbar_mult (Finite la) (Finite lb)) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Finite (Rmult la lb)) *)
    apply (Div2.ind_0_1_SS (fun n => (n <= S (2 * Div2.div2 n))%nat)).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply le_O_n.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply le_refl.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    move => k Hk.
(* Goal: le (S (S k)) (S (Init.Nat.mul (S (S O)) (Nat.div2 (S (S k))))) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Rbar_mult (Finite la) (Finite lb)) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Finite (Rmult la lb)) *)
    replace (Div2.div2 (S (S k))) with (S (Div2.div2 k)) by auto.
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult (Rminus (Series ap) (Series am)) (Rminus (Series bp) (Series bm))) *)
(* Goal: @eq R (Rminus (Series bp) (Series bm)) lb *)
(* Goal: @eq R (Rminus (Series ap) (Series am)) la *)
    replace (2 * S (Div2.div2 k))%nat with (S (S (2 * Div2.div2 k))) by ring.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by repeat apply le_n_S.

(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Finite (Rmult la lb)) *)
    apply is_lim_seq_mult'.
(* Goal: is_lim_seq (sum_f_R0 a) (Finite la) *)
(* Goal: is_lim_seq (sum_f_R0 b) (Finite lb) *)
    apply filterlim_ext with (2:=Hla); apply sum_n_Reals.
(* Goal: is_lim_seq (sum_f_R0 b) (Finite lb) *)
    apply filterlim_ext with (2:=Hlb); apply sum_n_Reals.
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Finite (Rmult la lb)) *)
    apply is_lim_seq_mult'.
(* Goal: is_lim_seq (sum_f_R0 a) (Finite la) *)
(* Goal: is_lim_seq (sum_f_R0 b) (Finite lb) *)
    apply filterlim_ext with (2:=Hla); apply sum_n_Reals.
(* Goal: is_lim_seq (sum_f_R0 b) (Finite lb) *)
    apply filterlim_ext with (2:=Hlb); apply sum_n_Reals.
Qed.

Lemma is_series_mult (a b : nat -> R) (la lb : R) :
  is_series  a la -> is_series  b lb
  -> ex_series  (fun n => Rabs (a n)) -> ex_series  (fun n => Rabs (b n))
  -> is_series  (fun n => sum_f_R0 (fun k => a k * b (n - k)%nat) n) (la * lb).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Hla Hlb Ha Hb.

(* Goal: False *)
  set ap := fun n => (a n + Rabs (a n)) / 2.
(* Goal: False *)
  set am := fun n => - (a n - Rabs (a n)) / 2.
(* Goal: False *)
  set bp := fun n => (b n + Rabs (b n)) / 2.
(* Goal: False *)
  set bm := fun n => - (b n - Rabs (b n)) / 2.

(* Goal: False *)
  have Hap : forall n, 0 <= ap n.
(* Goal: forall n : nat, Rle (IZR Z0) (bm n) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    move => n ; apply Rdiv_le_0_compat.
(* Goal: Rle (IZR Z0) (Rplus (b n) (Rabs (b n))) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    rewrite Rplus_comm ; apply Rle_minus_l ; rewrite Rminus_0_l.
(* Goal: Rle (Ropp (b n)) (Rabs (b n)) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply Rabs_maj2.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rlt_0_2.
  assert (Sap : ex_series  ap).
(* Goal: @ex_series R_AbsRing R_NormedModule bm *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply ex_series_scal_r.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    apply (@ex_series_plus ) => //.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by exists la.
(* Goal: False *)
  have Ham : forall n, 0 <= am n.
(* Goal: forall n : nat, Rle (IZR Z0) (bm n) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    move => n ; apply Rdiv_le_0_compat.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite Ropp_minus_distr'.
(* Goal: Rle (IZR Z0) (Rminus (Rabs (a n)) (a n)) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply (Rminus_le_0 (a _)).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rle_abs.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rlt_0_2.
  assert (Sam : ex_series  am).
(* Goal: @ex_series R_AbsRing R_NormedModule bm *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply ex_series_scal_r.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Ropp (Rminus (b n) (Rabs (b n)))) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply @ex_series_opp.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    apply @ex_series_minus => //.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by exists la.
(* Goal: False *)
  have Hbp : forall n, 0 <= bp n.
(* Goal: forall n : nat, Rle (IZR Z0) (bm n) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    move => n ; apply Rdiv_le_0_compat.
(* Goal: Rle (IZR Z0) (Rplus (b n) (Rabs (b n))) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    rewrite Rplus_comm ; apply Rle_minus_l ; rewrite Rminus_0_l.
(* Goal: Rle (Ropp (b n)) (Rabs (b n)) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply Rabs_maj2.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rlt_0_2.
  assert (Sbp : ex_series  bp).
(* Goal: @ex_series R_AbsRing R_NormedModule bm *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply ex_series_scal_r.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    apply @ex_series_plus => //.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by exists lb.
(* Goal: False *)
  have Hbm : forall n, 0 <= bm n.
(* Goal: forall n : nat, Rle (IZR Z0) (bm n) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    move => n ; apply Rdiv_le_0_compat.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite Ropp_minus_distr'.
(* Goal: Rle (IZR Z0) (Rminus (Rabs (b n)) (b n)) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply (Rminus_le_0 (b _)).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rle_abs.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rlt_0_2.
  assert (Sbm : ex_series  bm).
(* Goal: @ex_series R_AbsRing R_NormedModule bm *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply ex_series_scal_r.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Ropp (Rminus (b n) (Rabs (b n)))) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply @ex_series_opp.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    apply @ex_series_minus => //.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by exists lb.

  apply is_series_ext with (fun n => sum_f_R0 (fun k : nat => ap k * bp (n - k)%nat) n
    - sum_f_R0 (fun k : nat => am k * bp (n - k)%nat) n
    - sum_f_R0 (fun k : nat => ap k * bm (n - k)%nat) n
    + sum_f_R0 (fun k : nat => am k * bm (n - k)%nat) n).
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => n.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite -?minus_sum -plus_sum.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  apply sum_eq => k _.
(* Goal: @eq R (Rmult (@norm_factor K (CompleteNormedModule.NormedModule K V)) (Rdiv (pos eps) (@norm_factor K (CompleteNormedModule.NormedModule K V)))) (pos eps) *)
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a (S u) v)) (pos eps) *)
  rewrite /ap /am /bp /bm ; field.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => Rplus (Rminus (Rminus (sum_f_R0 (fun k : nat => Rmult (ap k) (bp (Init.Nat.sub n k))) n) (sum_f_R0 (fun k : nat => Rmult (am k) (bp (Init.Nat.sub n k))) n)) (sum_f_R0 (fun k : nat => Rmult (ap k) (bm (Init.Nat.sub n k))) n)) (sum_f_R0 (fun k : nat => Rmult (am k) (bm (Init.Nat.sub n k))) n)) (Rmult la lb) *)
  replace (la*lb) with ((Series ap*Series bp-Series am*Series bp-Series ap*Series bm)+Series am*Series bm).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => Rplus (Rminus (Rminus (sum_f_R0 (fun k : nat => Rmult (ap k) (bp (Init.Nat.sub n k))) n) (sum_f_R0 (fun k : nat => Rmult (am k) (bp (Init.Nat.sub n k))) n)) (sum_f_R0 (fun k : nat => Rmult (ap k) (bm (Init.Nat.sub n k))) n)) (sum_f_R0 (fun k : nat => Rmult (am k) (bm (Init.Nat.sub n k))) n)) (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) *)
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult la lb) *)
  apply @is_series_plus.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => Rminus (sum_f_R0 (fun k : nat => Rmult (ap k) (bp (Init.Nat.sub n k))) n) (sum_f_R0 (fun k : nat => Rmult (am k) (bp (Init.Nat.sub n k))) n)) (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (ap k) (bm (Init.Nat.sub n k))) n) (Rmult (Series ap) (Series bm)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (am k) (bm (Init.Nat.sub n k))) n) (Rmult (Series am) (Series bm)) *)
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult la lb) *)
  apply @is_series_minus.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => Rminus (sum_f_R0 (fun k : nat => Rmult (ap k) (bp (Init.Nat.sub n k))) n) (sum_f_R0 (fun k : nat => Rmult (am k) (bp (Init.Nat.sub n k))) n)) (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (ap k) (bm (Init.Nat.sub n k))) n) (Rmult (Series ap) (Series bm)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (am k) (bm (Init.Nat.sub n k))) n) (Rmult (Series am) (Series bm)) *)
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult la lb) *)
  apply @is_series_minus.
(* Goal: @is_series R_AbsRing R_NormedModule (fun k : nat => a (Init.Nat.add n k)) (Series (fun k : nat => a (Init.Nat.add n k))) *)
  apply is_series_mult_pos => // ; by apply Series_correct.
(* Goal: @is_series R_AbsRing R_NormedModule (fun k : nat => a (Init.Nat.add n k)) (Series (fun k : nat => a (Init.Nat.add n k))) *)
  apply is_series_mult_pos => // ; by apply Series_correct.
(* Goal: @is_series R_AbsRing R_NormedModule (fun k : nat => a (Init.Nat.add n k)) (Series (fun k : nat => a (Init.Nat.add n k))) *)
  apply is_series_mult_pos => // ; by apply Series_correct.
(* Goal: @is_series R_AbsRing R_NormedModule (fun k : nat => a (Init.Nat.add n k)) (Series (fun k : nat => a (Init.Nat.add n k))) *)
  apply is_series_mult_pos => // ; by apply Series_correct.
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult la lb) *)
  replace (la) with (Series ap - Series am).
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult (Rminus (Series ap) (Series am)) lb) *)
(* Goal: @eq R (Rminus (Series ap) (Series am)) la *)
  replace (lb) with (Series bp - Series bm).
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult (Rminus (Series ap) (Series am)) (Rminus (Series bp) (Series bm))) *)
(* Goal: @eq R (Rminus (Series bp) (Series bm)) lb *)
(* Goal: @eq R (Rminus (Series ap) (Series am)) la *)
  ring.
(* Goal: @eq R (Rminus (Series ap) (Series am)) la *)
  rewrite -Series_minus // -(is_series_unique _ _ Hlb) ; apply Series_ext => n.
(* Goal: @eq R (Rmult (@norm_factor K (CompleteNormedModule.NormedModule K V)) (Rdiv (pos eps) (@norm_factor K (CompleteNormedModule.NormedModule K V)))) (pos eps) *)
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a (S u) v)) (pos eps) *)
  rewrite /ap /am /bp /bm ; field.
(* Goal: @eq R (Rminus (Series ap) (Series am)) la *)
  rewrite -Series_minus // -(is_series_unique _ _ Hla) ; apply Series_ext => n.
(* Goal: @eq R (Rmult (@norm_factor K (CompleteNormedModule.NormedModule K V)) (Rdiv (pos eps) (@norm_factor K (CompleteNormedModule.NormedModule K V)))) (pos eps) *)
(* Goal: Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a (S u) v)) (pos eps) *)
  rewrite /ap /am /bp /bm ; field.
Qed.

(** * D'Alembert criterion *)

Lemma ex_series_DAlembert (a : nat -> R) (k : R) :
  k < 1 -> (forall n, a n <> 0)
    -> is_lim_seq (fun n => Rabs (a (S n) / a n)) k
      -> ex_series  (fun n => Rabs (a n)).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Hk Ha H.
(* Goal: False *)
  have : exists N, forall n, (N <= n)%nat -> Rabs (a (S n) / a n) <= (k+1)/2.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle (Rabs (Rdiv (a (S n)) (a n))) (Rdiv (Rplus k (IZR (Zpos xH))) (IZR (Zpos (xO xH))))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle (Rabs (Rdiv (a (S n)) (a n))) (Rdiv (Rplus k (IZR (Zpos xH))) (IZR (Zpos (xO xH))))), @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (a n)) *)
    apply is_lim_seq_spec in H.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    case: (fun He => H (mkposreal ((1-k)/2) He)).
      move: (fun He => is_pos_div_2 (mkposreal (1-k) He)) => /= He ;
      apply: He.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
      by apply -> Rminus_lt_0.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    move => {H} /= Hk1 N H.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    exists N => n Hn.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    move: (H n Hn) => {H} H.
    apply Rabs_lt_between' in H ; case: H => _ H ;
    field_simplify in H ; rewrite Rdiv_1 in H ; by apply Rlt_le.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case => {H} N H.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rabs (a n)) *)
  apply ex_series_incr_n with N.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun k : nat => Rabs (a (Init.Nat.add N k))) *)
  apply @ex_series_le with (fun n => Rabs (a N) * ((k+1)/2)^n).
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => n.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite /norm /= /abs /= Rabs_Rabsolu.
(* Goal: Rle (Rabs (a (Init.Nat.add N n))) (Rmult (Rabs (a N)) (pow (Rdiv (Rplus k (IZR (Zpos xH))) (IZR (Zpos (xO xH)))) n)) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rmult (Rabs (a N)) (pow (Rdiv (Rplus k (IZR (Zpos xH))) (IZR (Zpos (xO xH)))) n)) *)
  rewrite Rmult_comm ; apply Rle_div_l.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Rabs_pos_lt.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite -Rabs_div.
(* Goal: forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
  elim: n => [ | n IH].
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite plus_0_r /Rdiv Rinv_r.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  rewrite Rabs_R1 ; by apply Rle_refl.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Ha.
  replace (Rabs (a (N + S n)%nat / a N))
    with (Rabs (a (S (N + n))/a (N+n)%nat) * Rabs (a (N + n)%nat / a N)).
(* Goal: Rle (Rmult (Rabs (Rdiv (a (S (Init.Nat.add N n))) (a (Init.Nat.add N n)))) (Rabs (Rdiv (a (Init.Nat.add N n)) (a N)))) (pow (Rdiv (Rplus k (IZR (Zpos xH))) (IZR (Zpos (xO xH)))) (S n)) *)
(* Goal: @eq R (Rmult (Rabs (Rdiv (a (S (Init.Nat.add N n))) (a (Init.Nat.add N n)))) (Rabs (Rdiv (a (Init.Nat.add N n)) (a N)))) (Rabs (Rdiv (a (Init.Nat.add N (S n))) (a N))) *)
(* Goal: not (@eq R (a N) (IZR Z0)) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rmult (Rabs (a N)) (pow (Rdiv (Rplus k (IZR (Zpos xH))) (IZR (Zpos (xO xH)))) n)) *)
  simpl ; apply Rmult_le_compat.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Rabs_pos.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Rabs_pos.
(* Goal: Rle (Rabs (Rdiv (a (S (Init.Nat.add N n))) (a (Init.Nat.add N n)))) (Rdiv (Rplus k (IZR (Zpos xH))) (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rabs (Rdiv (a (Init.Nat.add N n)) (a N))) (pow (Rdiv (Rplus k (IZR (Zpos xH))) (IZR (Zpos (xO xH)))) n) *)
(* Goal: @eq R (Rmult (Rabs (Rdiv (a (S (Init.Nat.add N n))) (a (Init.Nat.add N n)))) (Rabs (Rdiv (a (Init.Nat.add N n)) (a N)))) (Rabs (Rdiv (a (Init.Nat.add N (S n))) (a N))) *)
(* Goal: not (@eq R (a N) (IZR Z0)) *)
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rmult (Rabs (a N)) (pow (Rdiv (Rplus k (IZR (Zpos xH))) (IZR (Zpos (xO xH)))) n)) *)
  apply H, le_plus_l.
(* Goal: @is_series K V (fun k : nat => a (S k)) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O))) *)
  by apply IH.
(* Goal: @eq R (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (Init.Nat.add (S k) O))) (b (Init.Nat.sub (S n) (S k))))) (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (S k))) (b (Init.Nat.sub (S (S n)) (S (S k)))))) *)
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) m) (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) (S m))))) (Rplus (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) m) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p))) (Init.Nat.add (S m) (S (S n))))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
  rewrite -Rabs_mult ; apply f_equal.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  rewrite plus_n_Sm ; field ; split ; by apply Ha.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Ha.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => Rmult (Rabs (a N)) (pow (Rdiv (Rplus k (IZR (Zpos xH))) (IZR (Zpos (xO xH)))) n)) *)
  apply @ex_series_scal_l.
(* Goal: False *)
  set k0 := ((k + 1) / 2).
(* Goal: @ex_series R_AbsRing R_NormedModule (pow k0) *)
  exists (/(1-k0) * (1-k0*0)).
(* Goal: @is_series R_AbsRing R_NormedModule (pow k0) (Rmult (Rinv (Rminus (IZR (Zpos xH)) k0)) (Rminus (IZR (Zpos xH)) (Rmult k0 (IZR Z0)))) *)
  apply filterlim_ext with (fun N => / (1 - k0) * (1 - k0 ^ S N)).
(* Goal: forall x : nat, @eq R (Rmult (Rinv (Rminus (IZR (Zpos xH)) k0)) (Rminus (IZR (Zpos xH)) (pow k0 (S x)))) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (pow k0) x) *)
(* Goal: @filterlim nat R (fun N : nat => Rmult (Rinv (Rminus (IZR (Zpos xH)) k0)) (Rminus (IZR (Zpos xH)) (pow k0 (S N)))) eventually (@locally (NormedModule.UniformSpace R_AbsRing R_NormedModule) (Rmult (Rinv (Rminus (IZR (Zpos xH)) k0)) (Rminus (IZR (Zpos xH)) (Rmult k0 (IZR Z0))))) *)
  move => n ; rewrite sum_n_Reals; rewrite tech3.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Rmult_comm.
(* Goal: Rlt k0 (IZR (Zpos xH)) *)
(* Goal: Rle (IZR Z0) k0 *)
(* Goal: is_Rbar_minus (Finite (IZR (Zpos xH))) (Finite (Rmult k0 (IZR Z0))) (Finite (Rminus (IZR (Zpos xH)) (Rmult k0 (IZR Z0)))) *)
  unfold k0 ; lra.
(* Goal: @filterlim nat R (fun N : nat => Rmult (Rinv (Rminus (IZR (Zpos xH)) k0)) (Rminus (IZR (Zpos xH)) (pow k0 (S N)))) eventually (@locally (NormedModule.UniformSpace R_AbsRing R_NormedModule) (Rmult (Rinv (Rminus (IZR (Zpos xH)) k0)) (Rminus (IZR (Zpos xH)) (Rmult k0 (IZR Z0))))) *)
  apply (is_lim_seq_scal_l (fun N0 => (1 - k0 ^ S N0)) (/ (1 - k0)) (Finite (1-k0*0))).
(* Goal: is_lim_seq (fun N0 : nat => Rminus (IZR (Zpos xH)) (pow k0 (S N0))) (Finite (Rminus (IZR (Zpos xH)) (Rmult k0 (IZR Z0)))) *)
  apply (is_lim_seq_minus _ _ (Finite 1) (Finite (k0*0))).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply is_lim_seq_const.
(* Goal: is_lim_seq (fun n : nat => pow k0 (S n)) (Finite (Rmult k0 (IZR Z0))) *)
(* Goal: is_Rbar_minus (Finite (IZR (Zpos xH))) (Finite (Rmult k0 (IZR Z0))) (Finite (Rminus (IZR (Zpos xH)) (Rmult k0 (IZR Z0)))) *)
  simpl pow ; apply (is_lim_seq_scal_l _ _ (Finite 0)).
(* Goal: is_lim_seq (pow k0) (Finite (IZR Z0)) *)
(* Goal: is_Rbar_minus (Finite (IZR (Zpos xH))) (Finite (Rmult k0 (IZR Z0))) (Finite (Rminus (IZR (Zpos xH)) (Rmult k0 (IZR Z0)))) *)
  apply (is_lim_seq_geom k0).
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite Rabs_pos_eq.
(* Goal: Rlt k0 (IZR (Zpos xH)) *)
(* Goal: Rle (IZR Z0) k0 *)
(* Goal: is_Rbar_minus (Finite (IZR (Zpos xH))) (Finite (Rmult k0 (IZR Z0))) (Finite (Rminus (IZR (Zpos xH)) (Rmult k0 (IZR Z0)))) *)
  unfold k0 ; lra.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  apply Rle_trans with (2 := H N (le_refl _)) ; by apply Rabs_pos.
(* Goal: is_Rbar_minus (Finite (IZR (Zpos xH))) (Finite (Rmult k0 (IZR Z0))) (Finite (Rminus (IZR (Zpos xH)) (Rmult k0 (IZR Z0)))) *)
  easy.
Qed.

Lemma not_ex_series_DAlembert (a : nat -> R) (l : R) :
  l > 1 -> (forall n, a n <> 0)
    -> is_lim_seq (fun n => Rabs (a (S n) / a n)) l
      -> ~ is_lim_seq a 0.
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Hl Ha Hda Ha0.
(* Goal: False *)
  set k := (l+1)/2.
(* Goal: False *)
  have Hk1 : 1 < k.
(* Goal: Rlt (IZR (Zpos xH)) k *)
(* Goal: False *)
    unfold k ; lra.
(* Goal: False *)
  have : exists N, forall n, (N <= n)%nat -> k <= Rabs (a (S n) / a n).
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    apply is_lim_seq_spec in Hda.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    case: (fun H => Hda (mkposreal ((l-1)/2) H)) => [ | /= {Hda} H N Hda].
(* Goal: Rlt (IZR Z0) (Rdiv (Rminus l (IZR (Zpos xH))) (IZR (Zpos (xO xH)))) *)
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    apply Rdiv_lt_0_compat.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply -> Rminus_lt_0.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rlt_R0_R2.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    exists N => n Hn.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    move: (Hda n Hn) => {Hda} Hda.
(* Goal: Rle k (Rabs (Rdiv (a (S n)) (a n))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    apply Rabs_lt_between' in Hda.
(* Goal: Rle k (Rabs (Rdiv (a (S n)) (a n))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
    replace (k) with (l - (l - 1) / 2) by (unfold k ; field).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rlt_le, Hda.
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case => N H.
(* Goal: False *)
  apply is_lim_seq_abs_0, (is_lim_seq_incr_n _ N) in Ha0.
(* Goal: False *)
  have : forall n, Rabs (a N) * k ^ n <= Rabs (a (n + N)%nat).
(* Goal: forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
    elim => /= [ | n IH].
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    rewrite Rmult_1_r ; by apply Rle_refl.
    replace (Rabs (a (S (n + N))))
      with (Rabs (a (S (n+N)) / a (n+N)%nat) * Rabs (a (n+N)%nat))
      by (rewrite -Rabs_mult ; apply f_equal ; by field).
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult (Rminus (Series ap) (Series am)) (Rminus (Series bp) (Series bm))) *)
(* Goal: @eq R (Rminus (Series bp) (Series bm)) lb *)
(* Goal: @eq R (Rminus (Series ap) (Series am)) la *)
    replace (Rabs (a N) * (k * k ^ n)) with (k * (Rabs (a N) * k ^ n)) by ring.
(* Goal: Rle (Rmult k (Rmult (Rabs (a N)) (pow k n))) (Rmult (Rabs (Rdiv (a (S (Init.Nat.add n N))) (a (Init.Nat.add n N)))) (Rabs (a (Init.Nat.add n N)))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
    apply Rmult_le_compat.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rlt_le, Rlt_trans with (1 := Rlt_0_1).
(* Goal: Rle (IZR Z0) (Rmult (Rabs (a N)) (pow k n)) *)
(* Goal: Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: is_lim_seq (fun _ : nat => IZR Z0) (Finite (IZR Z0)) *)
(* Goal: is_lim_seq (fun n : nat => Rabs (a (Init.Nat.add n N))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    apply Rmult_le_pos.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rabs_pos.
(* Goal: Rle (IZR Z0) (pow k n) *)
(* Goal: Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: is_lim_seq (fun _ : nat => IZR Z0) (Finite (IZR Z0)) *)
(* Goal: is_lim_seq (fun n : nat => Rabs (a (Init.Nat.add n N))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    apply pow_le.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rlt_le, Rlt_trans with (1 := Rlt_0_1).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply H, le_plus_r.
(* Goal: @is_series K V (fun k : nat => a (S k)) (@plus (NormedModule.AbelianGroup K V) l (@opp (NormedModule.AbelianGroup K V) (a O))) *)
    by apply IH.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => {H} H.
(* Goal: False *)
  have : Finite 0 = p_infty.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite -(Lim_seq_geom_p k Hk1).
(* Goal: @eq Rbar (Finite (IZR Z0)) (Lim_seq (fun n : nat => pow k n)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    apply sym_equal.
(* Goal: @eq Rbar (Lim_seq (fun n : nat => pow k n)) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    apply is_lim_seq_unique.
(* Goal: is_lim_seq (fun n : nat => pow k n) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    apply is_lim_seq_ext with (fun n => / Rabs (a N) * (Rabs (a N) * k ^ n)).
(* Goal: forall n : nat, @eq R (Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (pow k n) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    move => n ; field ; by apply Rabs_no_R0.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite -(Rmult_0_r (/Rabs (a N))).
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (Rmult (Rinv (Rabs (a N))) (IZR Z0))) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    apply (is_lim_seq_scal_l _ _ (Finite 0)).
(* Goal: is_lim_seq (fun n : nat => Rmult (Rabs (a N)) (pow k n)) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    apply is_lim_seq_le_le with (fun _ => 0) (fun n => Rabs (a (n + N)%nat)).
    move => n ; split.
(* Goal: Rle (IZR Z0) (Rmult (Rabs (a N)) (pow k n)) *)
(* Goal: Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: is_lim_seq (fun _ : nat => IZR Z0) (Finite (IZR Z0)) *)
(* Goal: is_lim_seq (fun n : nat => Rabs (a (Init.Nat.add n N))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    apply Rmult_le_pos.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rabs_pos.
(* Goal: Rle (IZR Z0) (pow k n) *)
(* Goal: Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: is_lim_seq (fun _ : nat => IZR Z0) (Finite (IZR Z0)) *)
(* Goal: is_lim_seq (fun n : nat => Rabs (a (Init.Nat.add n N))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    apply pow_le.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Rlt_le, Rlt_trans with (1 := Rlt_0_1).
(* Goal: Rlt (Rabs (Rminus (Rmult (sum_f_R0 a (Nat.div2 n)) (sum_f_R0 b (Nat.div2 n))) (Rmult la lb))) (pos eps) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Rbar_mult (Finite la) (Finite lb)) *)
(* Goal: is_lim_seq (fun n : nat => Rmult (sum_f_R0 a n) (sum_f_R0 b n)) (Finite (Rmult la lb)) *)
    by apply H.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply is_lim_seq_const.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
    by apply Ha0.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by [].
Qed.

Lemma partial_summation_R (a b : nat -> R) :
  (exists M, forall n, norm (sum_n b n) <= M)
  -> filterlim a eventually (locally 0)
  -> ex_series (fun n => norm (minus (a (S n)) (a n)))
  -> ex_series (fun n => scal (a n) (b n)).
Proof.
(* Goal: False *)
  set B := fun n => sum_n b n.
  intros Hb Ha0 Ha.
  eexists.
  unfold is_series.
  replace (@locally R_NormedModule)
    with (fun x => Rbar_locally (Finite x)) by auto.
  apply is_lim_seq_ext with (fun N =>
    plus (scal (a N) (B N))
    (match N with | O => zero | S N => sum_n (fun n => scal (minus (a n) (a (S n))) (B n)) N end)).
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case => /= [ | N].
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) l (@zero (NormedModule.AbelianGroup K V))) l *)
    rewrite /B /= !sum_O ; by apply plus_zero_r.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite sum_Sn plus_comm.
(* Goal: forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))) *)
(* Goal: forall _ : forall n : nat, Rle (Rmult (Rabs (a N)) (pow k n)) (Rabs (a (Init.Nat.add n N))), False *)
  elim: N => /= [ | N IH].
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite /B /= !sum_Sn !sum_O /minus !scal_distr_r !scal_distr_l !scal_opp_l.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite -!plus_assoc.
(* Goal: @eq R (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (Init.Nat.add (S k) O))) (b (Init.Nat.sub (S n) (S k))))) (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (S k))) (b (Init.Nat.sub (S (S n)) (S (S k)))))) *)
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) m) (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) (S m))))) (Rplus (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) m) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p))) (Init.Nat.add (S m) (S (S n))))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
    apply f_equal.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite plus_comm -!plus_assoc.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite plus_comm -!plus_assoc.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
    rewrite plus_opp_l.
(* Goal: @eq (AbelianGroup.sort (NormedModule.AbelianGroup K V)) (@plus (NormedModule.AbelianGroup K V) l (@zero (NormedModule.AbelianGroup K V))) l *)
    by apply plus_zero_r.
  rewrite !sum_Sn -IH ; clear IH.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite /B /= /minus !sum_Sn.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  generalize (sum_n (fun n : nat => scal (plus (a n) (opp (a (S n)))) (sum_n b n)) N) => /= c.
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  generalize (sum_n b N) => b'.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite !scal_distr_r !scal_distr_l -!plus_assoc !scal_opp_l.
(* Goal: @eq R (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (Init.Nat.add (S k) O))) (b (Init.Nat.sub (S n) (S k))))) (Rplus (sum_f_R0 (fun k : nat => Rmult (a (S k)) (b (Init.Nat.sub (S (S n)) (S k)))) k) (Rmult (a (S (S k))) (b (Init.Nat.sub (S (S n)) (S (S k)))))) *)
(* Goal: Rle (Rplus (sum_f_R0 (fun k : nat => sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l k))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) k))) m) (sum_f_R0 (fun l : nat => Rmult (a (S (Init.Nat.add l (S m)))) (b (Init.Nat.sub (S n) l))) (Init.Nat.pred (Init.Nat.sub (S n) (S m))))) (Rplus (sum_f_R0 (fun x : nat => sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add x (S (S n))) p))) (Init.Nat.add x (S (S n)))) m) (sum_f_R0 (fun p : nat => Rmult (a p) (b (Init.Nat.sub (Init.Nat.add (S m) (S (S n))) p))) (Init.Nat.add (S m) (S (S n))))) *)
(* Goal: @eq nat n (Init.Nat.sub (Init.Nat.add (S n) (S n)) (S (S n))) *)
(* Goal: lt (S n) (Init.Nat.add (S n) (S n)) *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
  repeat apply f_equal.
  repeat rewrite (plus_comm (scal (a (S (S N))) b')) -!plus_assoc.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite plus_comm -!plus_assoc plus_opp_r plus_zero_r.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by rewrite plus_assoc plus_opp_l plus_zero_l.
  apply is_lim_seq_plus'.
  instantiate (1 := 0).
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  apply filterlim_locally => eps.
  destruct Hb as [M Hb].
  eapply filter_imp.
  intros n Hn.
  apply @norm_compat1.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite /minus opp_zero plus_zero_r.
  eapply Rle_lt_trans.
  apply @norm_scal.
  eapply Rle_lt_trans.
  apply Rmult_le_compat_l.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply abs_ge_0.
  eapply Rle_trans.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Hb.
  apply (Rmax_r 1).
  apply Rlt_div_r.
  eapply Rlt_le_trans, Rmax_l.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Rlt_0_1.
  apply Hn.
  assert (0 < eps / Rmax 1 M).
(* Goal: Rlt (IZR Z0) (Rdiv (Rminus l (IZR (Zpos xH))) (IZR (Zpos (xO xH)))) *)
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  apply Rdiv_lt_0_compat.
(* Goal: Rlt (IZR Z0) (pos eps) *)
(* Goal: Rlt (IZR Z0) (@norm_factor K (CompleteNormedModule.NormedModule K V)) *)
(* Goal: @ex nat (fun N : nat => forall (n m : nat) (_ : le N n) (_ : le N m), Rlt (@norm K (CompleteNormedModule.NormedModule K V) (@sum_n_m (NormedModule.AbelianGroup K (CompleteNormedModule.NormedModule K V)) a n m)) (pos eps)) *)
  by apply eps.
  eapply Rlt_le_trans, Rmax_l.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Rlt_0_1.
  destruct (proj1 (filterlim_locally _ _) Ha0 (mkposreal _ H)) as [N HN].
(* Goal: @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))) *)
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  exists N => n Hn.
  eapply Rle_lt_trans, HN, Hn.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rinv (Rabs (a N))) (Rmult (Rabs (a N)) (pow k n))) (Finite (IZR Z0)) *)
(* Goal: forall _ : @eq Rbar (Finite (IZR Z0)) p_infty, False *)
  rewrite /minus opp_zero plus_zero_r.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Rle_refl.
  apply is_lim_seq_incr_1.
  apply (Lim_seq_correct' (fun n : nat =>
    sum_n (fun n0 : nat => scal (minus (a n0) (a (S n0))) (B n0)) n)).
(* Goal: forall _ : @ex nat (fun N : nat => forall (n : nat) (_ : le N n), Rle k (Rabs (Rdiv (a (S n)) (a n)))), False *)
  case: Hb => M Hb.
  eapply @ex_series_le.
(* Goal: forall n : nat, Rle (@norm R_AbsRing (CompleteNormedModule.NormedModule R_AbsRing R_CompleteNormedModule) (a n)) (b n) *)
(* Goal: @ex_series R_AbsRing R_NormedModule b *)
  intros n.
  eapply Rle_trans.
  apply @norm_scal.
  apply Rmult_le_compat_l.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply abs_ge_0.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply Hb.
(* Goal: @ex_series R_AbsRing R_NormedModule bm *)
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => sum_f_R0 (fun k : nat => Rmult (a k) (b (Init.Nat.sub n k))) n) (Rmult la lb) *)
  apply ex_series_scal_r.
  move: Ha ; apply ex_series_ext => n.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by rewrite -norm_opp /minus opp_plus opp_opp plus_comm.
Qed.

(** * Geometric series *)

Lemma is_series_geom (q : R) :
  Rabs q < 1 -> is_series  (fun n => q ^ n) (/ (1-q)).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Hq.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  apply filterlim_ext with (fun n => (1-q^(S n)) / (1-q)).
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => n.
(* Goal: @eq R (Rdiv (Rminus (IZR (Zpos xH)) (pow q (S n))) (Rminus (IZR (Zpos xH)) q)) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => pow q n) n) *)
(* Goal: @filterlim nat R (fun n : nat => Rdiv (Rminus (IZR (Zpos xH)) (pow q (S n))) (Rminus (IZR (Zpos xH)) q)) eventually (@locally (NormedModule.UniformSpace R_AbsRing R_NormedModule) (Rinv (Rminus (IZR (Zpos xH)) q))) *)
  rewrite sum_n_Reals; rewrite tech3.
(* Goal: @eq R (Rdiv (Rminus (IZR (Zpos xH)) (pow q (S n))) (Rminus (IZR (Zpos xH)) q)) (Rdiv (Rminus (IZR (Zpos xH)) (pow q (S n))) (Rminus (IZR (Zpos xH)) q)) *)
(* Goal: not (@eq R q (IZR (Zpos xH))) *)
(* Goal: @filterlim nat R (fun n : nat => Rdiv (Rminus (IZR (Zpos xH)) (pow q (S n))) (Rminus (IZR (Zpos xH)) q)) eventually (@locally (NormedModule.UniformSpace R_AbsRing R_NormedModule) (Rinv (Rminus (IZR (Zpos xH)) q))) *)
  reflexivity.
(* Goal: not (@eq R q (IZR (Zpos xH))) *)
(* Goal: @filterlim nat R (fun n : nat => Rdiv (Rminus (IZR (Zpos xH)) (pow q (S n))) (Rminus (IZR (Zpos xH)) q)) eventually (@locally (NormedModule.UniformSpace R_AbsRing R_NormedModule) (Rinv (Rminus (IZR (Zpos xH)) q))) *)
  apply Rlt_not_eq.
(* Goal: Rlt q (IZR (Zpos xH)) *)
(* Goal: @filterlim nat R (fun n : nat => Rdiv (Rminus (IZR (Zpos xH)) (pow q (S n))) (Rminus (IZR (Zpos xH)) q)) eventually (@locally (NormedModule.UniformSpace R_AbsRing R_NormedModule) (Rinv (Rminus (IZR (Zpos xH)) q))) *)
  apply Rle_lt_trans with (2 := Hq).
(* Goal: Rle q (Rabs q) *)
(* Goal: @filterlim nat R (fun n : nat => Rdiv (Rminus (IZR (Zpos xH)) (pow q (S n))) (Rminus (IZR (Zpos xH)) q)) eventually (@locally (NormedModule.UniformSpace R_AbsRing R_NormedModule) (Rinv (Rminus (IZR (Zpos xH)) q))) *)
  apply Rle_abs.
(* Goal: @filterlim nat R (fun n : nat => Rdiv (Rminus (IZR (Zpos xH)) (pow q (S n))) (Rminus (IZR (Zpos xH)) q)) eventually (@locally (NormedModule.UniformSpace R_AbsRing R_NormedModule) (Rinv (Rminus (IZR (Zpos xH)) q))) *)
  change (is_lim_seq (fun n : nat => (1 - q ^ S n) / (1 - q)) (/(1-q))).
(* Goal: is_lim_seq (fun n : nat => Rdiv (Rminus (IZR (Zpos xH)) (pow q (S n))) (Rminus (IZR (Zpos xH)) q)) (Finite (Rinv (Rminus (IZR (Zpos xH)) q))) *)
  replace ((/ (1 - q))) with (real (Rbar_mult (Rbar_minus 1 0) (/ (1 - q)))).
(* Goal: is_lim_seq (fun n : nat => Rdiv (Rminus (IZR (Zpos xH)) (pow q (S n))) (Rminus (IZR (Zpos xH)) q)) (Finite (real (Rbar_mult (Rbar_minus (Finite (IZR (Zpos xH))) (Finite (IZR Z0))) (Finite (Rinv (Rminus (IZR (Zpos xH)) q)))))) *)
(* Goal: @eq R (real (Rbar_mult (Rbar_minus (Finite (IZR (Zpos xH))) (Finite (IZR Z0))) (Finite (Rinv (Rminus (IZR (Zpos xH)) q))))) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  unfold Rdiv.
(* Goal: is_lim_seq (fun n : nat => Rmult (Rminus (IZR (Zpos xH)) (pow q (S n))) (Rinv (Rminus (IZR (Zpos xH)) q))) (Finite (real (Rbar_mult (Rbar_minus (Finite (IZR (Zpos xH))) (Finite (IZR Z0))) (Finite (Rinv (Rminus (IZR (Zpos xH)) q)))))) *)
(* Goal: @eq R (real (Rbar_mult (Rbar_minus (Finite (IZR (Zpos xH))) (Finite (IZR Z0))) (Finite (Rinv (Rminus (IZR (Zpos xH)) q))))) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  apply (is_lim_seq_scal_r (fun n : nat => (1 - q ^ S n)) (/ (1 - q)) (Rbar_minus 1 0)).
(* Goal: is_lim_seq (fun n : nat => Rminus (IZR (Zpos xH)) (pow q (S n))) (Rbar_minus (Finite (IZR (Zpos xH))) (Finite (IZR Z0))) *)
(* Goal: @eq R (real (Rbar_mult (Rbar_minus (Finite (IZR (Zpos xH))) (Finite (IZR Z0))) (Finite (Rinv (Rminus (IZR (Zpos xH)) q))))) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  apply is_lim_seq_minus'.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply is_lim_seq_const.
(* Goal: is_lim_seq (fun n : nat => pow q (S n)) (Finite (IZR Z0)) *)
(* Goal: @eq R (real (Rbar_mult (Rbar_minus (Finite (IZR (Zpos xH))) (Finite (IZR Z0))) (Finite (Rinv (Rminus (IZR (Zpos xH)) q))))) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  apply (is_lim_seq_incr_1 (fun n => q^n)).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply is_lim_seq_geom.
(* Goal: @eq R (Rplus (Rminus (Rminus (Rmult (Series ap) (Series bp)) (Rmult (Series am) (Series bp))) (Rmult (Series ap) (Series bm))) (Rmult (Series am) (Series bm))) (Rmult (Rminus (Series ap) (Series am)) (Rminus (Series bp) (Series bm))) *)
(* Goal: @eq R (Rminus (Series bp) (Series bm)) lb *)
(* Goal: @eq R (Rminus (Series ap) (Series am)) la *)
  simpl; ring.
Qed.
Lemma ex_series_geom (q : R) :
  Rabs q < 1 -> ex_series  (fun n => q ^ n).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Hq.
(* Goal: @ex_series R_AbsRing R_NormedModule (fun n : nat => pow q n) *)
  exists (/(1-q)).
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply is_series_geom.
Qed.
Lemma Series_geom (q : R) :
  Rabs q < 1 -> Series (fun n => q ^ n) = / (1-q).
Proof.
(* Goal: forall _ : Rlt (Rabs q) (IZR (Zpos xH)), @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  move => Hq.
(* Goal: @eq R (Series (fun n : nat => pow q n)) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  apply is_series_unique.
(* Goal: @is_series R_AbsRing R_NormedModule (fun n : nat => pow q n) (Rinv (Rminus (IZR (Zpos xH)) q)) *)
  by apply is_series_geom.
Qed.
