Ranalysis4.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

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

Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Rtrigo1.
Require Import Ranalysis1.
Require Import Ranalysis3.
Require Import Exp_prop.
Require Import MVT.
Local Open Scope R_scope.

(**********)
Lemma derivable_pt_inv :
  forall (f:R -> R) (x:R),
    f x <> 0 -> derivable_pt f x -> derivable_pt (/ f) x.forall (f : R -> R) (x : R),
f x <> 0 -> derivable_pt f x -> derivable_pt (/ f) x
Proof.forall (f : R -> R) (x : R),
f x <> 0 -> derivable_pt f x -> derivable_pt (/ f) x
  intros f x H X; cut (derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x).f:R -> R
x:R
H:f x <> 0
X:derivable_pt f x
(derivable_pt (fct_cte 1 / f) x ->
 derivable_pt (/ f) x) -> derivable_pt (/ f) x
f:R -> R
x:R
H:f x <> 0
X:derivable_pt f x
derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x
  intro X0; apply X0.f:R -> R
x:R
H:f x <> 0
X:derivable_pt f x
X0:derivable_pt (fct_cte 1 / f) x ->
derivable_pt (/ f) x
derivable_pt (fct_cte 1 / f) x
f:R -> R
x:R
H:f x <> 0
X:derivable_pt f x
derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x
  apply derivable_pt_div.f:R -> R
x:R
H:f x <> 0
X:derivable_pt f x
X0:derivable_pt (fct_cte 1 / f) x ->
derivable_pt (/ f) x
derivable_pt (fct_cte 1) x
f:R -> R
x:R
H:f x <> 0
X:derivable_pt f x
X0:derivable_pt (fct_cte 1 / f) x ->
derivable_pt (/ f) x
derivable_pt f x
f:R -> R
x:R
H:f x <> 0
X:derivable_pt f x
X0:derivable_pt (fct_cte 1 / f) x ->
derivable_pt (/ f) x
f x <> 0
f:R -> R
x:R
H:f x <> 0
X:derivable_pt f x
derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x
  apply derivable_pt_const.f:R -> R
x:R
H:f x <> 0
X:derivable_pt f x
X0:derivable_pt (fct_cte 1 / f) x ->
derivable_pt (/ f) x
derivable_pt f x
f:R -> R
x:R
H:f x <> 0
X:derivable_pt f x
X0:derivable_pt (fct_cte 1 / f) x ->
derivable_pt (/ f) x
f x <> 0
f:R -> R
x:R
H:f x <> 0
X:derivable_pt f x
derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x
  assumption.f:R -> R
x:R
H:f x <> 0
X:derivable_pt f x
X0:derivable_pt (fct_cte 1 / f) x ->
derivable_pt (/ f) x
f x <> 0
f:R -> R
x:R
H:f x <> 0
X:derivable_pt f x
derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x
  assumption.f:R -> R
x:R
H:f x <> 0
X:derivable_pt f x
derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x
  unfold div_fct, inv_fct, fct_cte; intros (x0,p);
    unfold derivable_pt; exists x0;
      unfold derivable_pt_abs; unfold derivable_pt_lim;
        unfold derivable_pt_abs in p; unfold derivable_pt_lim in p;
          intros; elim (p eps H0); intros; exists x1; intros;
            unfold Rdiv in H1; unfold Rdiv; rewrite <- (Rmult_1_l (/ f x));
              rewrite <- (Rmult_1_l (/ f (x + h))).f:R -> R
x:R
H:f x <> 0
X:derivable_pt f x
x0:R
p:forall eps0 : R,
0 < eps0 ->
exists delta : posreal,
  forall h0 : R,
  h0 <> 0 ->
  Rabs h0 < delta ->
  Rabs ((1 / f (x + h0) - 1 / f x) / h0 - x0) <
  eps0
eps:R
H0:0 < eps
x1:posreal
H1:forall h0 : R,
h0 <> 0 ->
Rabs h0 < x1 ->
Rabs ((1 * / f (x + h0) - 1 * / f x) * / h0 - x0) <
eps
h:R
H2:h <> 0
H3:Rabs h < x1
Rabs ((1 * / f (x + h) - 1 * / f x) * / h - x0) < eps
  apply H1; assumption.
Qed.

(**********)
Lemma pr_nu_var :
  forall (f g:R -> R) (x:R) (pr1:derivable_pt f x) (pr2:derivable_pt g x),
    f = g -> derive_pt f x pr1 = derive_pt g x pr2.forall (f g : R -> R) (x : R) (pr1 : derivable_pt f x)
  (pr2 : derivable_pt g x),
f = g -> derive_pt f x pr1 = derive_pt g x pr2
Proof.forall (f g : R -> R) (x : R) (pr1 : derivable_pt f x)
  (pr2 : derivable_pt g x),
f = g -> derive_pt f x pr1 = derive_pt g x pr2
  unfold derivable_pt, derive_pt; intros f g x (x0,p0) (x1,p1) ->.g:R -> R
x, x0:R
p0:derivable_pt_abs g x x0
x1:R
p1:derivable_pt_abs g x x1
proj1_sig
  (exist (fun l : R => derivable_pt_abs g x l) x0 p0) =
proj1_sig
  (exist (fun l : R => derivable_pt_abs g x l) x1 p1)
  apply uniqueness_limite with g x; assumption.
Qed.

(**********)
Lemma pr_nu_var2 :
  forall (f g:R -> R) (x:R) (pr1:derivable_pt f x) (pr2:derivable_pt g x),
    (forall h:R, f h = g h) -> derive_pt f x pr1 = derive_pt g x pr2.forall (f g : R -> R) (x : R) (pr1 : derivable_pt f x)
  (pr2 : derivable_pt g x),
(forall h : R, f h = g h) ->
derive_pt f x pr1 = derive_pt g x pr2
Proof.forall (f g : R -> R) (x : R) (pr1 : derivable_pt f x)
  (pr2 : derivable_pt g x),
(forall h : R, f h = g h) ->
derive_pt f x pr1 = derive_pt g x pr2
  unfold derivable_pt, derive_pt; intros f g x (x0,p0) (x1,p1) H.f, g:R -> R
x, x0:R
p0:derivable_pt_abs f x x0
x1:R
p1:derivable_pt_abs g x x1
H:forall h : R, f h = g h
proj1_sig
  (exist (fun l : R => derivable_pt_abs f x l) x0 p0) =
proj1_sig
  (exist (fun l : R => derivable_pt_abs g x l) x1 p1)
  assert (H0 := uniqueness_step2 _ _ _ p0).f, g:R -> R
x, x0:R
p0:derivable_pt_abs f x x0
x1:R
p1:derivable_pt_abs g x x1
H:forall h : R, f h = g h
H0:limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x0 0
proj1_sig
  (exist (fun l : R => derivable_pt_abs f x l) x0 p0) =
proj1_sig
  (exist (fun l : R => derivable_pt_abs g x l) x1 p1)
  assert (H1 := uniqueness_step2 _ _ _ p1).f, g:R -> R
x, x0:R
p0:derivable_pt_abs f x x0
x1:R
p1:derivable_pt_abs g x x1
H:forall h : R, f h = g h
H0:limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x0 0
H1:limit1_in (fun h : R => (g (x + h) - g x) / h)
  (fun h : R => h <> 0) x1 0
proj1_sig
  (exist (fun l : R => derivable_pt_abs f x l) x0 p0) =
proj1_sig
  (exist (fun l : R => derivable_pt_abs g x l) x1 p1)
  cut (limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) x1 0).f, g:R -> R
x, x0:R
p0:derivable_pt_abs f x x0
x1:R
p1:derivable_pt_abs g x x1
H:forall h : R, f h = g h
H0:limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x0 0
H1:limit1_in (fun h : R => (g (x + h) - g x) / h)
  (fun h : R => h <> 0) x1 0
limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x1 0 ->
proj1_sig
  (exist (fun l : R => derivable_pt_abs f x l) x0 p0) =
proj1_sig
  (exist (fun l : R => derivable_pt_abs g x l) x1 p1)
f, g:R -> R
x, x0:R
p0:derivable_pt_abs f x x0
x1:R
p1:derivable_pt_abs g x x1
H:forall h : R, f h = g h
H0:limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x0 0
H1:limit1_in (fun h : R => (g (x + h) - g x) / h)
  (fun h : R => h <> 0) x1 0
limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x1 0
  intro H2; assert (H3 := uniqueness_step1 _ _ _ _ H0 H2).f, g:R -> R
x, x0:R
p0:derivable_pt_abs f x x0
x1:R
p1:derivable_pt_abs g x x1
H:forall h : R, f h = g h
H0:limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x0 0
H1:limit1_in (fun h : R => (g (x + h) - g x) / h)
  (fun h : R => h <> 0) x1 0
H2:limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x1 0
H3:x0 = x1
proj1_sig
  (exist (fun l : R => derivable_pt_abs f x l) x0 p0) =
proj1_sig
  (exist (fun l : R => derivable_pt_abs g x l) x1 p1)
f, g:R -> R
x, x0:R
p0:derivable_pt_abs f x x0
x1:R
p1:derivable_pt_abs g x x1
H:forall h : R, f h = g h
H0:limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x0 0
H1:limit1_in (fun h : R => (g (x + h) - g x) / h)
  (fun h : R => h <> 0) x1 0
limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x1 0
  assumption.f, g:R -> R
x, x0:R
p0:derivable_pt_abs f x x0
x1:R
p1:derivable_pt_abs g x x1
H:forall h : R, f h = g h
H0:limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x0 0
H1:limit1_in (fun h : R => (g (x + h) - g x) / h)
  (fun h : R => h <> 0) x1 0
limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x1 0
  unfold limit1_in; unfold limit_in; unfold dist;
    simpl; unfold R_dist; unfold limit1_in in H1;
      unfold limit_in in H1; unfold dist in H1; simpl in H1;
        unfold R_dist in H1.f, g:R -> R
x, x0:R
p0:derivable_pt_abs f x x0
x1:R
p1:derivable_pt_abs g x x1
H:forall h : R, f h = g h
H0:limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x0 0
H1:forall eps : R,
eps > 0 ->
exists alp : R,
  alp > 0 /\
  (forall x2 : R,
   x2 <> 0 /\ Rabs (x2 - 0) < alp ->
   Rabs ((g (x + x2) - g x) / x2 - x1) < eps)
forall eps : R,
eps > 0 ->
exists alp : R,
  alp > 0 /\
  (forall x2 : R,
   x2 <> 0 /\ Rabs (x2 - 0) < alp ->
   Rabs ((f (x + x2) - f x) / x2 - x1) < eps)
  intros; elim (H1 eps H2); intros.f, g:R -> R
x, x0:R
p0:derivable_pt_abs f x x0
x1:R
p1:derivable_pt_abs g x x1
H:forall h : R, f h = g h
H0:limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x0 0
H1:forall eps0 : R,
eps0 > 0 ->
exists alp : R,
  alp > 0 /\
  (forall x3 : R,
   x3 <> 0 /\ Rabs (x3 - 0) < alp ->
   Rabs ((g (x + x3) - g x) / x3 - x1) < eps0)
eps:R
H2:eps > 0
x2:R
H3:x2 > 0 /\
(forall x3 : R,
 x3 <> 0 /\ Rabs (x3 - 0) < x2 ->
 Rabs ((g (x + x3) - g x) / x3 - x1) < eps)
exists alp : R,
  alp > 0 /\
  (forall x3 : R,
   x3 <> 0 /\ Rabs (x3 - 0) < alp ->
   Rabs ((f (x + x3) - f x) / x3 - x1) < eps)
  elim H3; intros.f, g:R -> R
x, x0:R
p0:derivable_pt_abs f x x0
x1:R
p1:derivable_pt_abs g x x1
H:forall h : R, f h = g h
H0:limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x0 0
H1:forall eps0 : R,
eps0 > 0 ->
exists alp : R,
  alp > 0 /\
  (forall x3 : R,
   x3 <> 0 /\ Rabs (x3 - 0) < alp ->
   Rabs ((g (x + x3) - g x) / x3 - x1) < eps0)
eps:R
H2:eps > 0
x2:R
H3:x2 > 0 /\
(forall x3 : R,
 x3 <> 0 /\ Rabs (x3 - 0) < x2 ->
 Rabs ((g (x + x3) - g x) / x3 - x1) < eps)
H4:x2 > 0
H5:forall x3 : R,
x3 <> 0 /\ Rabs (x3 - 0) < x2 ->
Rabs ((g (x + x3) - g x) / x3 - x1) < eps
exists alp : R,
  alp > 0 /\
  (forall x3 : R,
   x3 <> 0 /\ Rabs (x3 - 0) < alp ->
   Rabs ((f (x + x3) - f x) / x3 - x1) < eps)
  exists x2.f, g:R -> R
x, x0:R
p0:derivable_pt_abs f x x0
x1:R
p1:derivable_pt_abs g x x1
H:forall h : R, f h = g h
H0:limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x0 0
H1:forall eps0 : R,
eps0 > 0 ->
exists alp : R,
  alp > 0 /\
  (forall x3 : R,
   x3 <> 0 /\ Rabs (x3 - 0) < alp ->
   Rabs ((g (x + x3) - g x) / x3 - x1) < eps0)
eps:R
H2:eps > 0
x2:R
H3:x2 > 0 /\
(forall x3 : R,
 x3 <> 0 /\ Rabs (x3 - 0) < x2 ->
 Rabs ((g (x + x3) - g x) / x3 - x1) < eps)
H4:x2 > 0
H5:forall x3 : R,
x3 <> 0 /\ Rabs (x3 - 0) < x2 ->
Rabs ((g (x + x3) - g x) / x3 - x1) < eps
x2 > 0 /\
(forall x3 : R,
 x3 <> 0 /\ Rabs (x3 - 0) < x2 ->
 Rabs ((f (x + x3) - f x) / x3 - x1) < eps)
  split.f, g:R -> R
x, x0:R
p0:derivable_pt_abs f x x0
x1:R
p1:derivable_pt_abs g x x1
H:forall h : R, f h = g h
H0:limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x0 0
H1:forall eps0 : R,
eps0 > 0 ->
exists alp : R,
  alp > 0 /\
  (forall x3 : R,
   x3 <> 0 /\ Rabs (x3 - 0) < alp ->
   Rabs ((g (x + x3) - g x) / x3 - x1) < eps0)
eps:R
H2:eps > 0
x2:R
H3:x2 > 0 /\
(forall x3 : R,
 x3 <> 0 /\ Rabs (x3 - 0) < x2 ->
 Rabs ((g (x + x3) - g x) / x3 - x1) < eps)
H4:x2 > 0
H5:forall x3 : R,
x3 <> 0 /\ Rabs (x3 - 0) < x2 ->
Rabs ((g (x + x3) - g x) / x3 - x1) < eps
x2 > 0
f, g:R -> R
x, x0:R
p0:derivable_pt_abs f x x0
x1:R
p1:derivable_pt_abs g x x1
H:forall h : R, f h = g h
H0:limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x0 0
H1:forall eps0 : R,
eps0 > 0 ->
exists alp : R,
  alp > 0 /\
  (forall x3 : R,
   x3 <> 0 /\ Rabs (x3 - 0) < alp ->
   Rabs ((g (x + x3) - g x) / x3 - x1) < eps0)
eps:R
H2:eps > 0
x2:R
H3:x2 > 0 /\
(forall x3 : R,
 x3 <> 0 /\ Rabs (x3 - 0) < x2 ->
 Rabs ((g (x + x3) - g x) / x3 - x1) < eps)
H4:x2 > 0
H5:forall x3 : R,
x3 <> 0 /\ Rabs (x3 - 0) < x2 ->
Rabs ((g (x + x3) - g x) / x3 - x1) < eps
forall x3 : R,
x3 <> 0 /\ Rabs (x3 - 0) < x2 ->
Rabs ((f (x + x3) - f x) / x3 - x1) < eps
  assumption.f, g:R -> R
x, x0:R
p0:derivable_pt_abs f x x0
x1:R
p1:derivable_pt_abs g x x1
H:forall h : R, f h = g h
H0:limit1_in (fun h : R => (f (x + h) - f x) / h)
  (fun h : R => h <> 0) x0 0
H1:forall eps0 : R,
eps0 > 0 ->
exists alp : R,
  alp > 0 /\
  (forall x3 : R,
   x3 <> 0 /\ Rabs (x3 - 0) < alp ->
   Rabs ((g (x + x3) - g x) / x3 - x1) < eps0)
eps:R
H2:eps > 0
x2:R
H3:x2 > 0 /\
(forall x3 : R,
 x3 <> 0 /\ Rabs (x3 - 0) < x2 ->
 Rabs ((g (x + x3) - g x) / x3 - x1) < eps)
H4:x2 > 0
H5:forall x3 : R,
x3 <> 0 /\ Rabs (x3 - 0) < x2 ->
Rabs ((g (x + x3) - g x) / x3 - x1) < eps
forall x3 : R,
x3 <> 0 /\ Rabs (x3 - 0) < x2 ->
Rabs ((f (x + x3) - f x) / x3 - x1) < eps
  intros; do 2 rewrite H; apply H5; assumption.
Qed.

(**********)
Lemma derivable_inv :
  forall f:R -> R, (forall x:R, f x <> 0) -> derivable f -> derivable (/ f).forall f : R -> R,
(forall x : R, f x <> 0) ->
derivable f -> derivable (/ f)
Proof.forall f : R -> R,
(forall x : R, f x <> 0) ->
derivable f -> derivable (/ f)
  intros f H X.f:R -> R
H:forall x : R, f x <> 0
X:derivable f
derivable (/ f)
  unfold derivable; intro x.f:R -> R
H:forall x0 : R, f x0 <> 0
X:derivable f
x:R
derivable_pt (/ f) x
  apply derivable_pt_inv.f:R -> R
H:forall x0 : R, f x0 <> 0
X:derivable f
x:R
f x <> 0
f:R -> R
H:forall x0 : R, f x0 <> 0
X:derivable f
x:R
derivable_pt f x
  apply (H x).f:R -> R
H:forall x0 : R, f x0 <> 0
X:derivable f
x:R
derivable_pt f x
  apply (X x).
Qed.

Lemma derive_pt_inv :
  forall (f:R -> R) (x:R) (pr:derivable_pt f x) (na:f x <> 0),
    derive_pt (/ f) x (derivable_pt_inv f x na pr) =
    - derive_pt f x pr / Rsqr (f x).forall (f : R -> R) (x : R) (pr : derivable_pt f x)
  (na : f x <> 0),
derive_pt (/ f) x (derivable_pt_inv f x na pr) =
- derive_pt f x pr / (f x)²
Proof.forall (f : R -> R) (x : R) (pr : derivable_pt f x)
  (na : f x <> 0),
derive_pt (/ f) x (derivable_pt_inv f x na pr) =
- derive_pt f x pr / (f x)²
  intros;
    replace (derive_pt (/ f) x (derivable_pt_inv f x na pr)) with
    (derive_pt (fct_cte 1 / f) x
      (derivable_pt_div (fct_cte 1) f x (derivable_pt_const 1 x) pr na)).f:R -> R
x:R
pr:derivable_pt f x
na:f x <> 0
derive_pt (fct_cte 1 / f) x
  (derivable_pt_div (fct_cte 1) f x
     (derivable_pt_const 1 x) pr na) =
- derive_pt f x pr / (f x)²
f:R -> R
x:R
pr:derivable_pt f x
na:f x <> 0
derive_pt (fct_cte 1 / f) x
  (derivable_pt_div (fct_cte 1) f x
     (derivable_pt_const 1 x) pr na) =
derive_pt (/ f) x (derivable_pt_inv f x na pr)
  rewrite derive_pt_div; rewrite derive_pt_const; unfold fct_cte;
    rewrite Rmult_0_l; rewrite Rmult_1_r; unfold Rminus;
      rewrite Rplus_0_l; reflexivity.f:R -> R
x:R
pr:derivable_pt f x
na:f x <> 0
derive_pt (fct_cte 1 / f) x
  (derivable_pt_div (fct_cte 1) f x
     (derivable_pt_const 1 x) pr na) =
derive_pt (/ f) x (derivable_pt_inv f x na pr)
  apply pr_nu_var2.f:R -> R
x:R
pr:derivable_pt f x
na:f x <> 0
forall h : R, (fct_cte 1 / f)%F h = (/ f)%F h
  intro; unfold div_fct, fct_cte, inv_fct.f:R -> R
x:R
pr:derivable_pt f x
na:f x <> 0
h:R
1 / f h = / f h
  unfold Rdiv; ring.
Qed.

Rabsolu

Lemma Rabs_derive_1 : forall x:R, 0 < x -> derivable_pt_lim Rabs x 1.forall x : R, 0 < x -> derivable_pt_lim Rabs x 1
Proof.forall x : R, 0 < x -> derivable_pt_lim Rabs x 1
  intros.x:R
H:0 < x
derivable_pt_lim Rabs x 1
  unfold derivable_pt_lim; intros.x:R
H:0 < x
eps:R
H0:0 < eps
exists delta : posreal,
  forall h : R,
  h <> 0 ->
  Rabs h < delta ->
  Rabs ((Rabs (x + h) - Rabs x) / h - 1) < eps
  exists (mkposreal x H); intros.x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
Rabs ((Rabs (x + h) - Rabs x) / h - 1) < eps
  rewrite (Rabs_right x).x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
Rabs ((Rabs (x + h) - x) / h - 1) < eps
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x >= 0
  rewrite (Rabs_right (x + h)).x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
Rabs ((x + h - x) / h - 1) < eps
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x + h >= 0
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x >= 0
  rewrite Rplus_comm.x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
Rabs ((h + x - x) / h - 1) < eps
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x + h >= 0
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x >= 0
  unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_r.x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
Rabs ((h + 0) / h + - (1)) < eps
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x + h >= 0
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x >= 0
  rewrite Rplus_0_r; unfold Rdiv; rewrite <- Rinv_r_sym.x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
Rabs (1 + - (1)) < eps
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
h <> 0
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x + h >= 0
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x >= 0
  rewrite Rplus_opp_r; rewrite Rabs_R0; apply H0.x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
h <> 0
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x + h >= 0
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x >= 0
  apply H1.x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x + h >= 0
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x >= 0
  apply Rle_ge.x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
0 <= x + h
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x >= 0
  destruct (Rcase_abs h) as [Hlt|Hgt].x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
Hlt:h < 0
0 <= x + h
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
Hgt:h >= 0
0 <= x + h
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x >= 0
  rewrite (Rabs_left h Hlt) in H2.x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:- h < {| pos := x; cond_pos := H |}
Hlt:h < 0
0 <= x + h
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
Hgt:h >= 0
0 <= x + h
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x >= 0
  left; rewrite Rplus_comm; apply Rplus_lt_reg_l with (- h); rewrite Rplus_0_r;
    rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l;
      apply H2.x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
Hgt:h >= 0
0 <= x + h
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x >= 0
  apply Rplus_le_le_0_compat.x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
Hgt:h >= 0
0 <= x
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
Hgt:h >= 0
0 <= h
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x >= 0
  left; apply H.x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
Hgt:h >= 0
0 <= h
x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x >= 0
  apply Rge_le; apply Hgt.x:R
H:0 < x
eps:R
H0:0 < eps
h:R
H1:h <> 0
H2:Rabs h < {| pos := x; cond_pos := H |}
x >= 0
  left; apply H.
Qed.

Lemma Rabs_derive_2 : forall x:R, x < 0 -> derivable_pt_lim Rabs x (-1).forall x : R, x < 0 -> derivable_pt_lim Rabs x (-1)
Proof.forall x : R, x < 0 -> derivable_pt_lim Rabs x (-1)
  intros.x:R
H:x < 0
derivable_pt_lim Rabs x (-1)
  unfold derivable_pt_lim; intros.x:R
H:x < 0
eps:R
H0:0 < eps
exists delta : posreal,
  forall h : R,
  h <> 0 ->
  Rabs h < delta ->
  Rabs ((Rabs (x + h) - Rabs x) / h - -1) < eps
  cut (0 < - x).x:R
H:x < 0
eps:R
H0:0 < eps
0 < - x ->
exists delta : posreal,
  forall h : R,
  h <> 0 ->
  Rabs h < delta ->
  Rabs ((Rabs (x + h) - Rabs x) / h - -1) < eps
x:R
H:x < 0
eps:R
H0:0 < eps
0 < - x
  intro; exists (mkposreal (- x) H1); intros.x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
Rabs ((Rabs (x + h) - Rabs x) / h - -1) < eps
x:R
H:x < 0
eps:R
H0:0 < eps
0 < - x
  rewrite (Rabs_left x).x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
Rabs ((Rabs (x + h) - - x) / h - -1) < eps
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
x < 0
x:R
H:x < 0
eps:R
H0:0 < eps
0 < - x
  rewrite (Rabs_left (x + h)).x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
Rabs ((- (x + h) - - x) / h - -1) < eps
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
x + h < 0
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
x < 0
x:R
H:x < 0
eps:R
H0:0 < eps
0 < - x
  replace ((-(x + h) - - x) / h - -1) with 0 by now field.x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
Rabs 0 < eps
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
x + h < 0
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
x < 0
x:R
H:x < 0
eps:R
H0:0 < eps
0 < - x
  rewrite Rabs_R0; apply H0.x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
x + h < 0
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
x < 0
x:R
H:x < 0
eps:R
H0:0 < eps
0 < - x
  destruct (Rcase_abs h) as [Hlt|Hgt].x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
Hlt:h < 0
x + h < 0
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
Hgt:h >= 0
x + h < 0
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
x < 0
x:R
H:x < 0
eps:R
H0:0 < eps
0 < - x
  apply Ropp_lt_cancel.x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
Hlt:h < 0
- 0 < - (x + h)
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
Hgt:h >= 0
x + h < 0
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
x < 0
x:R
H:x < 0
eps:R
H0:0 < eps
0 < - x
  rewrite Ropp_0; rewrite Ropp_plus_distr; apply Rplus_lt_0_compat.x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
Hlt:h < 0
0 < - x
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
Hlt:h < 0
0 < - h
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
Hgt:h >= 0
x + h < 0
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
x < 0
x:R
H:x < 0
eps:R
H0:0 < eps
0 < - x
  apply H1.x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
Hlt:h < 0
0 < - h
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
Hgt:h >= 0
x + h < 0
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
x < 0
x:R
H:x < 0
eps:R
H0:0 < eps
0 < - x
  apply Ropp_0_gt_lt_contravar; apply Hlt.x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
Hgt:h >= 0
x + h < 0
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
x < 0
x:R
H:x < 0
eps:R
H0:0 < eps
0 < - x
  rewrite (Rabs_right h Hgt) in H3.x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:h < {| pos := - x; cond_pos := H1 |}
Hgt:h >= 0
x + h < 0
x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
x < 0
x:R
H:x < 0
eps:R
H0:0 < eps
0 < - x
  apply Rplus_lt_reg_l with (- x); rewrite Rplus_0_r; rewrite <- Rplus_assoc;
    rewrite Rplus_opp_l; rewrite Rplus_0_l; apply H3.x:R
H:x < 0
eps:R
H0:0 < eps
H1:0 < - x
h:R
H2:h <> 0
H3:Rabs h < {| pos := - x; cond_pos := H1 |}
x < 0
x:R
H:x < 0
eps:R
H0:0 < eps
0 < - x
  apply H.x:R
H:x < 0
eps:R
H0:0 < eps
0 < - x
  apply Ropp_0_gt_lt_contravar; apply H.
Qed.

Rabsolu is derivable for all x <> 0

Lemma Rderivable_pt_abs : forall x:R, x <> 0 -> derivable_pt Rabs x.forall x : R, x <> 0 -> derivable_pt Rabs x
Proof.forall x : R, x <> 0 -> derivable_pt Rabs x
  intros.x:R
H:x <> 0
derivable_pt Rabs x
  destruct (total_order_T x 0) as [[Hlt|Heq]|Hgt].x:R
H:x <> 0
Hlt:x < 0
derivable_pt Rabs x
x:R
H:x <> 0
Heq:x = 0
derivable_pt Rabs x
x:R
H:x <> 0
Hgt:x > 0
derivable_pt Rabs x
  unfold derivable_pt; exists (-1).x:R
H:x <> 0
Hlt:x < 0
derivable_pt_abs Rabs x (-1)
x:R
H:x <> 0
Heq:x = 0
derivable_pt Rabs x
x:R
H:x <> 0
Hgt:x > 0
derivable_pt Rabs x
  apply (Rabs_derive_2 x Hlt).x:R
H:x <> 0
Heq:x = 0
derivable_pt Rabs x
x:R
H:x <> 0
Hgt:x > 0
derivable_pt Rabs x
  elim H; exact Heq.x:R
H:x <> 0
Hgt:x > 0
derivable_pt Rabs x
  unfold derivable_pt; exists 1.x:R
H:x <> 0
Hgt:x > 0
derivable_pt_abs Rabs x 1
  apply (Rabs_derive_1 x Hgt).
Qed.

Rabsolu is continuous for all x

Lemma Rcontinuity_abs : continuity Rabs.continuity Rabs
Proof.continuity Rabs
  unfold continuity; intro.x:R
continuity_pt Rabs x
  case (Req_dec x 0); intro.x:R
H:x = 0
continuity_pt Rabs x
x:R
H:x <> 0
continuity_pt Rabs x
  unfold continuity_pt; unfold continue_in;
    unfold limit1_in; unfold limit_in;
      simpl; unfold R_dist; intros; exists eps;
        split.x:R
H:x = 0
eps:R
H0:eps > 0
eps > 0
x:R
H:x = 0
eps:R
H0:eps > 0
forall x0 : R,
D_x no_cond x x0 /\ Rabs (x0 - x) < eps ->
Rabs (Rabs x0 - Rabs x) < eps
x:R
H:x <> 0
continuity_pt Rabs x
  apply H0.x:R
H:x = 0
eps:R
H0:eps > 0
forall x0 : R,
D_x no_cond x x0 /\ Rabs (x0 - x) < eps ->
Rabs (Rabs x0 - Rabs x) < eps
x:R
H:x <> 0
continuity_pt Rabs x
  intros; rewrite H; rewrite Rabs_R0; unfold Rminus; rewrite Ropp_0;
    rewrite Rplus_0_r; rewrite Rabs_Rabsolu; elim H1;
      intros; rewrite H in H3; unfold Rminus in H3; rewrite Ropp_0 in H3;
        rewrite Rplus_0_r in H3; apply H3.x:R
H:x <> 0
continuity_pt Rabs x
  apply derivable_continuous_pt; apply (Rderivable_pt_abs x H).
Qed.

Finite sums : Sum a_k x^k

Lemma continuity_finite_sum :
  forall (An:nat -> R) (N:nat),
    continuity (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N).forall (An : nat -> R) (N : nat),
continuity
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N)
Proof.forall (An : nat -> R) (N : nat),
continuity
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N)
  intros; unfold continuity; intro.An:nat -> R
N:nat
x:R
continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  induction  N as [| N HrecN].An:nat -> R
x:R
continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) 0) x
An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  simpl.An:nat -> R
x:R
continuity_pt (fun _ : R => An 0%nat * 1) x
An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  apply continuity_pt_const.An:nat -> R
x:R
constant (fun _ : R => An 0%nat * 1)
An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  unfold constant; intros; reflexivity.An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  replace (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) (S N)) with
  ((fun y:R => sum_f_R0 (fun k:nat => (An k * y ^ k)%R) N) +
    (fun y:R => (An (S N) * y ^ S N)%R))%F.An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
continuity_pt
  ((fun y : R =>
    sum_f_R0 (fun k : nat => An k * y ^ k) N) +
   (fun y : R => An (S N) * y ^ S N)) x
An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
  apply continuity_pt_plus.An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
continuity_pt (fun y : R => An (S N) * y ^ S N) x
An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
  apply HrecN.An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
continuity_pt (fun y : R => An (S N) * y ^ S N) x
An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
  replace (fun y:R => An (S N) * y ^ S N) with
  (mult_real_fct (An (S N)) (fun y:R => y ^ S N)).An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
continuity_pt
  (mult_real_fct (An (S N)) (fun y : R => y ^ S N)) x
An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
mult_real_fct (An (S N)) (fun y : R => y ^ S N) =
(fun y : R => An (S N) * y ^ S N)
An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
  apply continuity_pt_scal.An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
continuity_pt (fun y : R => y ^ S N) x
An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
mult_real_fct (An (S N)) (fun y : R => y ^ S N) =
(fun y : R => An (S N) * y ^ S N)
An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
  apply derivable_continuous_pt.An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
derivable_pt (fun y : R => y ^ S N) x
An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
mult_real_fct (An (S N)) (fun y : R => y ^ S N) =
(fun y : R => An (S N) * y ^ S N)
An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
  apply derivable_pt_pow.An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
mult_real_fct (An (S N)) (fun y : R => y ^ S N) =
(fun y : R => An (S N) * y ^ S N)
An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
  reflexivity.An:nat -> R
N:nat
x:R
HrecN:continuity_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
  reflexivity.
Qed.

Lemma derivable_pt_lim_fs :
  forall (An:nat -> R) (x:R) (N:nat),
    (0 < N)%nat ->
    derivable_pt_lim (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N) x
    (sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred N)).forall (An : nat -> R) (x : R) (N : nat),
(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
Proof.forall (An : nat -> R) (x : R) (N : nat),
(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
  intros; induction  N as [| N HrecN].An:nat -> R
x:R
H:(0 < 0)%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) 0) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred 0))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
  elim (lt_irrefl _ H).An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
  cut (N = 0%nat \/ (0 < N)%nat).An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  intro; elim H0; intro.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  rewrite H1.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) 1) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred 1))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  simpl.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
derivable_pt_lim
  (fun y : R => An 0%nat * 1 + An 1%nat * (y * 1)) x
  (1 * An 1%nat * 1)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  replace (fun y:R => An 0%nat * 1 + An 1%nat * (y * 1)) with
  (fct_cte (An 0%nat * 1) + mult_real_fct (An 1%nat) (id * fct_cte 1))%F.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
derivable_pt_lim
  (fct_cte (An 0%nat * 1) +
   mult_real_fct (An 1%nat) (id * fct_cte 1)) x
  (1 * An 1%nat * 1)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
(fct_cte (An 0%nat * 1) +
 mult_real_fct (An 1%nat) (id * fct_cte 1))%F =
(fun y : R => An 0%nat * 1 + An 1%nat * (y * 1))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  replace (1 * An 1%nat * 1) with (0 + An 1%nat * (1 * fct_cte 1 x + id x * 0)).An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
derivable_pt_lim
  (fct_cte (An 0%nat * 1) +
   mult_real_fct (An 1%nat) (id * fct_cte 1)) x
  (0 + An 1%nat * (1 * fct_cte 1 x + id x * 0))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
0 + An 1%nat * (1 * fct_cte 1 x + id x * 0) =
1 * An 1%nat * 1
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
(fct_cte (An 0%nat * 1) +
 mult_real_fct (An 1%nat) (id * fct_cte 1))%F =
(fun y : R => An 0%nat * 1 + An 1%nat * (y * 1))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  apply derivable_pt_lim_plus.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
derivable_pt_lim (fct_cte (An 0%nat * 1)) x 0
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
derivable_pt_lim
  (mult_real_fct (An 1%nat) (id * fct_cte 1)) x
  (An 1%nat * (1 * fct_cte 1 x + id x * 0))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
0 + An 1%nat * (1 * fct_cte 1 x + id x * 0) =
1 * An 1%nat * 1
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
(fct_cte (An 0%nat * 1) +
 mult_real_fct (An 1%nat) (id * fct_cte 1))%F =
(fun y : R => An 0%nat * 1 + An 1%nat * (y * 1))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  apply derivable_pt_lim_const.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
derivable_pt_lim
  (mult_real_fct (An 1%nat) (id * fct_cte 1)) x
  (An 1%nat * (1 * fct_cte 1 x + id x * 0))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
0 + An 1%nat * (1 * fct_cte 1 x + id x * 0) =
1 * An 1%nat * 1
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
(fct_cte (An 0%nat * 1) +
 mult_real_fct (An 1%nat) (id * fct_cte 1))%F =
(fun y : R => An 0%nat * 1 + An 1%nat * (y * 1))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  apply derivable_pt_lim_scal.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
derivable_pt_lim (id * fct_cte 1) x
  (1 * fct_cte 1 x + id x * 0)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
0 + An 1%nat * (1 * fct_cte 1 x + id x * 0) =
1 * An 1%nat * 1
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
(fct_cte (An 0%nat * 1) +
 mult_real_fct (An 1%nat) (id * fct_cte 1))%F =
(fun y : R => An 0%nat * 1 + An 1%nat * (y * 1))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  apply derivable_pt_lim_mult.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
derivable_pt_lim id x 1
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
derivable_pt_lim (fct_cte 1) x 0
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
0 + An 1%nat * (1 * fct_cte 1 x + id x * 0) =
1 * An 1%nat * 1
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
(fct_cte (An 0%nat * 1) +
 mult_real_fct (An 1%nat) (id * fct_cte 1))%F =
(fun y : R => An 0%nat * 1 + An 1%nat * (y * 1))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  apply derivable_pt_lim_id.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
derivable_pt_lim (fct_cte 1) x 0
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
0 + An 1%nat * (1 * fct_cte 1 x + id x * 0) =
1 * An 1%nat * 1
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
(fct_cte (An 0%nat * 1) +
 mult_real_fct (An 1%nat) (id * fct_cte 1))%F =
(fun y : R => An 0%nat * 1 + An 1%nat * (y * 1))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  apply derivable_pt_lim_const.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
0 + An 1%nat * (1 * fct_cte 1 x + id x * 0) =
1 * An 1%nat * 1
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
(fct_cte (An 0%nat * 1) +
 mult_real_fct (An 1%nat) (id * fct_cte 1))%F =
(fun y : R => An 0%nat * 1 + An 1%nat * (y * 1))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  unfold fct_cte, id; ring.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:N = 0%nat
(fct_cte (An 0%nat * 1) +
 mult_real_fct (An 1%nat) (id * fct_cte 1))%F =
(fun y : R => An 0%nat * 1 + An 1%nat * (y * 1))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  reflexivity.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  replace (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) (S N)) with
  ((fun y:R => sum_f_R0 (fun k:nat => (An k * y ^ k)%R) N) +
    (fun y:R => (An (S N) * y ^ S N)%R))%F.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  ((fun y : R =>
    sum_f_R0 (fun k : nat => An k * y ^ k) N) +
   (fun y : R => An (S N) * y ^ S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  replace (sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred (S N)))
    with
      (sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred N) +
        An (S N) * (INR (S (pred (S N))) * x ^ pred (S N))).An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  ((fun y : R =>
    sum_f_R0 (fun k : nat => An k * y ^ k) N) +
   (fun y : R => An (S N) * y ^ S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N) +
   An (S N) *
   (INR (S (Init.Nat.pred (S N))) *
    x ^ Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred N) +
An (S N) *
(INR (S (Init.Nat.pred (S N))) *
 x ^ Init.Nat.pred (S N)) =
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  apply derivable_pt_lim_plus.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim (fun y : R => An (S N) * y ^ S N) x
  (An (S N) *
   (INR (S (Init.Nat.pred (S N))) *
    x ^ Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred N) +
An (S N) *
(INR (S (Init.Nat.pred (S N))) *
 x ^ Init.Nat.pred (S N)) =
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  apply HrecN.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
(0 < N)%nat
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim (fun y : R => An (S N) * y ^ S N) x
  (An (S N) *
   (INR (S (Init.Nat.pred (S N))) *
    x ^ Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred N) +
An (S N) *
(INR (S (Init.Nat.pred (S N))) *
 x ^ Init.Nat.pred (S N)) =
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  assumption.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim (fun y : R => An (S N) * y ^ S N) x
  (An (S N) *
   (INR (S (Init.Nat.pred (S N))) *
    x ^ Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred N) +
An (S N) *
(INR (S (Init.Nat.pred (S N))) *
 x ^ Init.Nat.pred (S N)) =
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  replace (fun y:R => An (S N) * y ^ S N) with
  (mult_real_fct (An (S N)) (fun y:R => y ^ S N)).An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim
  (mult_real_fct (An (S N)) (fun y : R => y ^ S N)) x
  (An (S N) *
   (INR (S (Init.Nat.pred (S N))) *
    x ^ Init.Nat.pred (S N)))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
mult_real_fct (An (S N)) (fun y : R => y ^ S N) =
(fun y : R => An (S N) * y ^ S N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred N) +
An (S N) *
(INR (S (Init.Nat.pred (S N))) *
 x ^ Init.Nat.pred (S N)) =
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  apply derivable_pt_lim_scal.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim (fun y : R => y ^ S N) x
  (INR (S (Init.Nat.pred (S N))) *
   x ^ Init.Nat.pred (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
mult_real_fct (An (S N)) (fun y : R => y ^ S N) =
(fun y : R => An (S N) * y ^ S N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred N) +
An (S N) *
(INR (S (Init.Nat.pred (S N))) *
 x ^ Init.Nat.pred (S N)) =
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  replace (pred (S N)) with N; [ idtac | reflexivity ].An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim (fun y : R => y ^ S N) x
  (INR (S N) * x ^ N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
mult_real_fct (An (S N)) (fun y : R => y ^ S N) =
(fun y : R => An (S N) * y ^ S N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred N) +
An (S N) *
(INR (S (Init.Nat.pred (S N))) *
 x ^ Init.Nat.pred (S N)) =
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  pattern N at 3; replace N with (pred (S N)).An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
derivable_pt_lim (fun y : R => y ^ S N) x
  (INR (S N) * x ^ Init.Nat.pred (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
Init.Nat.pred (S N) = N
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
mult_real_fct (An (S N)) (fun y : R => y ^ S N) =
(fun y : R => An (S N) * y ^ S N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred N) +
An (S N) *
(INR (S (Init.Nat.pred (S N))) *
 x ^ Init.Nat.pred (S N)) =
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  apply derivable_pt_lim_pow.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
Init.Nat.pred (S N) = N
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
mult_real_fct (An (S N)) (fun y : R => y ^ S N) =
(fun y : R => An (S N) * y ^ S N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred N) +
An (S N) *
(INR (S (Init.Nat.pred (S N))) *
 x ^ Init.Nat.pred (S N)) =
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  reflexivity.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
mult_real_fct (An (S N)) (fun y : R => y ^ S N) =
(fun y : R => An (S N) * y ^ S N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred N) +
An (S N) *
(INR (S (Init.Nat.pred (S N))) *
 x ^ Init.Nat.pred (S N)) =
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  reflexivity.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred N) +
An (S N) *
(INR (S (Init.Nat.pred (S N))) *
 x ^ Init.Nat.pred (S N)) =
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  cut (pred (S N) = S (pred N)).An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
Init.Nat.pred (S N) = S (Init.Nat.pred N) ->
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred N) +
An (S N) *
(INR (S (Init.Nat.pred (S N))) *
 x ^ Init.Nat.pred (S N)) =
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
Init.Nat.pred (S N) = S (Init.Nat.pred N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  intro; rewrite H2.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
H2:Init.Nat.pred (S N) = S (Init.Nat.pred N)
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred N) +
An (S N) *
(INR (S (S (Init.Nat.pred N))) *
 x ^ S (Init.Nat.pred N)) =
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (S (Init.Nat.pred N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
Init.Nat.pred (S N) = S (Init.Nat.pred N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  rewrite tech5.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
H2:Init.Nat.pred (S N) = S (Init.Nat.pred N)
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred N) +
An (S N) *
(INR (S (S (Init.Nat.pred N))) *
 x ^ S (Init.Nat.pred N)) =
sum_f_R0 (fun k : nat => INR (S k) * An (S k) * x ^ k)
  (Init.Nat.pred N) +
INR (S (S (Init.Nat.pred N))) *
An (S (S (Init.Nat.pred N))) * 
x ^ S (Init.Nat.pred N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
Init.Nat.pred (S N) = S (Init.Nat.pred N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  apply Rplus_eq_compat_l.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
H2:Init.Nat.pred (S N) = S (Init.Nat.pred N)
An (S N) *
(INR (S (S (Init.Nat.pred N))) *
 x ^ S (Init.Nat.pred N)) =
INR (S (S (Init.Nat.pred N))) *
An (S (S (Init.Nat.pred N))) * 
x ^ S (Init.Nat.pred N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
Init.Nat.pred (S N) = S (Init.Nat.pred N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  rewrite <- H2.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
H2:Init.Nat.pred (S N) = S (Init.Nat.pred N)
An (S N) *
(INR (S (Init.Nat.pred (S N))) *
 x ^ Init.Nat.pred (S N)) =
INR (S (Init.Nat.pred (S N))) *
An (S (Init.Nat.pred (S N))) * 
x ^ Init.Nat.pred (S N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
Init.Nat.pred (S N) = S (Init.Nat.pred N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  replace (pred (S N)) with N; [ idtac | reflexivity ].An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
H2:Init.Nat.pred (S N) = S (Init.Nat.pred N)
An (S N) * (INR (S N) * x ^ N) =
INR (S N) * An (S N) * x ^ N
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
Init.Nat.pred (S N) = S (Init.Nat.pred N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  ring.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
Init.Nat.pred (S N) = S (Init.Nat.pred N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  simpl.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
N = S (Init.Nat.pred N)
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  apply S_pred with 0%nat; assumption.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
((fun y : R =>
  sum_f_R0 (fun k : nat => (An k * y ^ k)%R) N) +
 (fun y : R => (An (S N) * y ^ S N)%R))%F =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  unfold plus_fct.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H0:N = 0%nat \/ (0 < N)%nat
H1:(0 < N)%nat
(fun x0 : R =>
 sum_f_R0 (fun k : nat => An k * x0 ^ k) N +
 An (S N) * x0 ^ S N) =
(fun y : R =>
 sum_f_R0 (fun k : nat => An k * y ^ k) (S N))
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  simpl; reflexivity.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
N = 0%nat \/ (0 < N)%nat
  inversion H.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
H1:0%nat = N
0%nat = 0%nat \/ (0 < 0)%nat
An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
m:nat
H1:(1 <= N)%nat
H0:m = N
N = 0%nat \/ (0 < N)%nat
  left; reflexivity.An:nat -> R
x:R
N:nat
H:(0 < S N)%nat
HrecN:(0 < N)%nat ->
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  (sum_f_R0
     (fun k : nat =>
      INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred N))
m:nat
H1:(1 <= N)%nat
H0:m = N
N = 0%nat \/ (0 < N)%nat
  right; apply lt_le_trans with 1%nat; [ apply lt_O_Sn | assumption ].
Qed.

Lemma derivable_pt_lim_finite_sum :
  forall (An:nat -> R) (x:R) (N:nat),
    derivable_pt_lim (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N) x
    match N with
      | O => 0
      | _ => sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred N)
    end.forall (An : nat -> R) (x : R) (N : nat),
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  match N with
  | 0%nat => 0
  | S _ =>
      sum_f_R0
        (fun k : nat => INR (S k) * An (S k) * x ^ k)
        (Init.Nat.pred N)
  end
Proof.forall (An : nat -> R) (x : R) (N : nat),
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  match N with
  | 0%nat => 0
  | S _ =>
      sum_f_R0
        (fun k : nat => INR (S k) * An (S k) * x ^ k)
        (Init.Nat.pred N)
  end
  intros.An:nat -> R
x:R
N:nat
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  match N with
  | 0%nat => 0
  | S _ =>
      sum_f_R0
        (fun k : nat => INR (S k) * An (S k) * x ^ k)
        (Init.Nat.pred N)
  end
  induction  N as [| N HrecN].An:nat -> R
x:R
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) 0) x 0
An:nat -> R
x:R
N:nat
HrecN:derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  match N with
  | 0%nat => 0
  | S _ =>
      sum_f_R0
        (fun k : nat =>
         INR (S k) * An (S k) * x ^ k)
        (Init.Nat.pred N)
  end
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
  simpl.An:nat -> R
x:R
derivable_pt_lim (fun _ : R => An 0%nat * 1) x 0
An:nat -> R
x:R
N:nat
HrecN:derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  match N with
  | 0%nat => 0
  | S _ =>
      sum_f_R0
        (fun k : nat =>
         INR (S k) * An (S k) * x ^ k)
        (Init.Nat.pred N)
  end
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
  rewrite Rmult_1_r.An:nat -> R
x:R
derivable_pt_lim (fun _ : R => An 0%nat) x 0
An:nat -> R
x:R
N:nat
HrecN:derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  match N with
  | 0%nat => 0
  | S _ =>
      sum_f_R0
        (fun k : nat =>
         INR (S k) * An (S k) * x ^ k)
        (Init.Nat.pred N)
  end
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
  replace (fun _:R => An 0%nat) with (fct_cte (An 0%nat));
  [ apply derivable_pt_lim_const | reflexivity ].An:nat -> R
x:R
N:nat
HrecN:derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  match N with
  | 0%nat => 0
  | S _ =>
      sum_f_R0
        (fun k : nat =>
         INR (S k) * An (S k) * x ^ k)
        (Init.Nat.pred N)
  end
derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
  apply derivable_pt_lim_fs; apply lt_O_Sn.
Qed.

Lemma derivable_pt_finite_sum :
  forall (An:nat -> R) (N:nat) (x:R),
    derivable_pt (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N) x.forall (An : nat -> R) (N : nat) (x : R),
derivable_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
Proof.forall (An : nat -> R) (N : nat) (x : R),
derivable_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  intros.An:nat -> R
N:nat
x:R
derivable_pt
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  unfold derivable_pt.An:nat -> R
N:nat
x:R
{l : R |
derivable_pt_abs
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x l}
  assert (H := derivable_pt_lim_finite_sum An x N).An:nat -> R
N:nat
x:R
H:derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  match N with
  | 0%nat => 0
  | S _ =>
      sum_f_R0
        (fun k : nat =>
         INR (S k) * An (S k) * x ^ k)
        (Init.Nat.pred N)
  end
{l : R |
derivable_pt_abs
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x l}
  induction  N as [| N HrecN].An:nat -> R
x:R
H:derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) 0) x 0
{l : R |
derivable_pt_abs
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) 0) x l}
An:nat -> R
N:nat
x:R
H:derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
HrecN:derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  match N with
  | 0%nat => 0
  | S _ =>
      sum_f_R0
        (fun k : nat =>
         INR (S k) * An (S k) * x ^ k)
        (Init.Nat.pred N)
  end ->
{l : R |
derivable_pt_abs
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  l}
{l : R |
derivable_pt_abs
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x l}
  exists 0; apply H.An:nat -> R
N:nat
x:R
H:derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x
  (sum_f_R0
     (fun k : nat => INR (S k) * An (S k) * x ^ k)
     (Init.Nat.pred (S N)))
HrecN:derivable_pt_lim
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  match N with
  | 0%nat => 0
  | S _ =>
      sum_f_R0
        (fun k : nat =>
         INR (S k) * An (S k) * x ^ k)
        (Init.Nat.pred N)
  end ->
{l : R |
derivable_pt_abs
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N) x
  l}
{l : R |
derivable_pt_abs
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) (S N)) x l}
  exists
    (sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred (S N)));
    apply H.
Qed.

Lemma derivable_finite_sum :
  forall (An:nat -> R) (N:nat),
    derivable (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N).forall (An : nat -> R) (N : nat),
derivable
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N)
Proof.forall (An : nat -> R) (N : nat),
derivable
  (fun y : R =>
   sum_f_R0 (fun k : nat => An k * y ^ k) N)
  intros; unfold derivable; intro; apply derivable_pt_finite_sum.
Qed.

Regularity of hyperbolic functions

Lemma derivable_pt_lim_cosh : forall x:R, derivable_pt_lim cosh x (sinh x).forall x : R, derivable_pt_lim cosh x (sinh x)
Proof.forall x : R, derivable_pt_lim cosh x (sinh x)
  intro.x:R
derivable_pt_lim cosh x (sinh x)
  unfold cosh, sinh; unfold Rdiv.x:R
derivable_pt_lim
  (fun x0 : R => (exp x0 + exp (- x0)) * / 2) x
  ((exp x - exp (- x)) * / 2)
  replace (fun x0:R => (exp x0 + exp (- x0)) * / 2) with
  ((exp + comp exp (- id)) * fct_cte (/ 2))%F; [ idtac | reflexivity ].x:R
derivable_pt_lim
  ((exp + comp exp (- id)) * fct_cte (/ 2)) x
  ((exp x - exp (- x)) * / 2)
  replace ((exp x - exp (- x)) * / 2) with
  ((exp x + exp (- x) * -1) * fct_cte (/ 2) x +
    (exp + comp exp (- id))%F x * 0).x:R
derivable_pt_lim
  ((exp + comp exp (- id)) * fct_cte (/ 2)) x
  ((exp x + exp (- x) * -1) * fct_cte (/ 2) x +
   (exp + comp exp (- id))%F x * 0)
x:R
(exp x + exp (- x) * -1) * fct_cte (/ 2) x +
(exp + comp exp (- id))%F x * 0 =
(exp x - exp (- x)) * / 2
  apply derivable_pt_lim_mult.x:R
derivable_pt_lim (exp + comp exp (- id)) x
  (exp x + exp (- x) * -1)
x:R
derivable_pt_lim (fct_cte (/ 2)) x 0
x:R
(exp x + exp (- x) * -1) * fct_cte (/ 2) x +
(exp + comp exp (- id))%F x * 0 =
(exp x - exp (- x)) * / 2
  apply derivable_pt_lim_plus.x:R
derivable_pt_lim exp x (exp x)
x:R
derivable_pt_lim (comp exp (- id)) x (exp (- x) * -1)
x:R
derivable_pt_lim (fct_cte (/ 2)) x 0
x:R
(exp x + exp (- x) * -1) * fct_cte (/ 2) x +
(exp + comp exp (- id))%F x * 0 =
(exp x - exp (- x)) * / 2
  apply derivable_pt_lim_exp.x:R
derivable_pt_lim (comp exp (- id)) x (exp (- x) * -1)
x:R
derivable_pt_lim (fct_cte (/ 2)) x 0
x:R
(exp x + exp (- x) * -1) * fct_cte (/ 2) x +
(exp + comp exp (- id))%F x * 0 =
(exp x - exp (- x)) * / 2
  apply derivable_pt_lim_comp.x:R
derivable_pt_lim (- id) x (-1)
x:R
derivable_pt_lim exp ((- id)%F x) (exp (- x))
x:R
derivable_pt_lim (fct_cte (/ 2)) x 0
x:R
(exp x + exp (- x) * -1) * fct_cte (/ 2) x +
(exp + comp exp (- id))%F x * 0 =
(exp x - exp (- x)) * / 2
  apply derivable_pt_lim_opp.x:R
derivable_pt_lim id x (IPR 1)
x:R
derivable_pt_lim exp ((- id)%F x) (exp (- x))
x:R
derivable_pt_lim (fct_cte (/ 2)) x 0
x:R
(exp x + exp (- x) * -1) * fct_cte (/ 2) x +
(exp + comp exp (- id))%F x * 0 =
(exp x - exp (- x)) * / 2
  apply derivable_pt_lim_id.x:R
derivable_pt_lim exp ((- id)%F x) (exp (- x))
x:R
derivable_pt_lim (fct_cte (/ 2)) x 0
x:R
(exp x + exp (- x) * -1) * fct_cte (/ 2) x +
(exp + comp exp (- id))%F x * 0 =
(exp x - exp (- x)) * / 2
  apply derivable_pt_lim_exp.x:R
derivable_pt_lim (fct_cte (/ 2)) x 0
x:R
(exp x + exp (- x) * -1) * fct_cte (/ 2) x +
(exp + comp exp (- id))%F x * 0 =
(exp x - exp (- x)) * / 2
  apply derivable_pt_lim_const.x:R
(exp x + exp (- x) * -1) * fct_cte (/ 2) x +
(exp + comp exp (- id))%F x * 0 =
(exp x - exp (- x)) * / 2
  unfold plus_fct, mult_real_fct, comp, opp_fct, id, fct_cte; ring.
Qed.

Lemma derivable_pt_lim_sinh : forall x:R, derivable_pt_lim sinh x (cosh x).forall x : R, derivable_pt_lim sinh x (cosh x)
Proof.forall x : R, derivable_pt_lim sinh x (cosh x)
  intro.x:R
derivable_pt_lim sinh x (cosh x)
  unfold cosh, sinh; unfold Rdiv.x:R
derivable_pt_lim
  (fun x0 : R => (exp x0 - exp (- x0)) * / 2) x
  ((exp x + exp (- x)) * / 2)
  replace (fun x0:R => (exp x0 - exp (- x0)) * / 2) with
  ((exp - comp exp (- id)) * fct_cte (/ 2))%F; [ idtac | reflexivity ].x:R
derivable_pt_lim
  ((exp - comp exp (- id)) * fct_cte (/ 2)) x
  ((exp x + exp (- x)) * / 2)
  replace ((exp x + exp (- x)) * / 2) with
  ((exp x - exp (- x) * -1) * fct_cte (/ 2) x +
    (exp - comp exp (- id))%F x * 0).x:R
derivable_pt_lim
  ((exp - comp exp (- id)) * fct_cte (/ 2)) x
  ((exp x - exp (- x) * -1) * fct_cte (/ 2) x +
   (exp - comp exp (- id))%F x * 0)
x:R
(exp x - exp (- x) * -1) * fct_cte (/ 2) x +
(exp - comp exp (- id))%F x * 0 =
(exp x + exp (- x)) * / 2
  apply derivable_pt_lim_mult.x:R
derivable_pt_lim (exp - comp exp (- id)) x
  (exp x - exp (- x) * -1)
x:R
derivable_pt_lim (fct_cte (/ 2)) x 0
x:R
(exp x - exp (- x) * -1) * fct_cte (/ 2) x +
(exp - comp exp (- id))%F x * 0 =
(exp x + exp (- x)) * / 2
  apply derivable_pt_lim_minus.x:R
derivable_pt_lim exp x (exp x)
x:R
derivable_pt_lim (comp exp (- id)) x (exp (- x) * -1)
x:R
derivable_pt_lim (fct_cte (/ 2)) x 0
x:R
(exp x - exp (- x) * -1) * fct_cte (/ 2) x +
(exp - comp exp (- id))%F x * 0 =
(exp x + exp (- x)) * / 2
  apply derivable_pt_lim_exp.x:R
derivable_pt_lim (comp exp (- id)) x (exp (- x) * -1)
x:R
derivable_pt_lim (fct_cte (/ 2)) x 0
x:R
(exp x - exp (- x) * -1) * fct_cte (/ 2) x +
(exp - comp exp (- id))%F x * 0 =
(exp x + exp (- x)) * / 2
  apply derivable_pt_lim_comp.x:R
derivable_pt_lim (- id) x (-1)
x:R
derivable_pt_lim exp ((- id)%F x) (exp (- x))
x:R
derivable_pt_lim (fct_cte (/ 2)) x 0
x:R
(exp x - exp (- x) * -1) * fct_cte (/ 2) x +
(exp - comp exp (- id))%F x * 0 =
(exp x + exp (- x)) * / 2
  apply derivable_pt_lim_opp.x:R
derivable_pt_lim id x (IPR 1)
x:R
derivable_pt_lim exp ((- id)%F x) (exp (- x))
x:R
derivable_pt_lim (fct_cte (/ 2)) x 0
x:R
(exp x - exp (- x) * -1) * fct_cte (/ 2) x +
(exp - comp exp (- id))%F x * 0 =
(exp x + exp (- x)) * / 2
  apply derivable_pt_lim_id.x:R
derivable_pt_lim exp ((- id)%F x) (exp (- x))
x:R
derivable_pt_lim (fct_cte (/ 2)) x 0
x:R
(exp x - exp (- x) * -1) * fct_cte (/ 2) x +
(exp - comp exp (- id))%F x * 0 =
(exp x + exp (- x)) * / 2
  apply derivable_pt_lim_exp.x:R
derivable_pt_lim (fct_cte (/ 2)) x 0
x:R
(exp x - exp (- x) * -1) * fct_cte (/ 2) x +
(exp - comp exp (- id))%F x * 0 =
(exp x + exp (- x)) * / 2
  apply derivable_pt_lim_const.x:R
(exp x - exp (- x) * -1) * fct_cte (/ 2) x +
(exp - comp exp (- id))%F x * 0 =
(exp x + exp (- x)) * / 2
  unfold plus_fct, mult_real_fct, comp, opp_fct, id, fct_cte; ring.
Qed.

Lemma derivable_pt_exp : forall x:R, derivable_pt exp x.forall x : R, derivable_pt exp x
Proof.forall x : R, derivable_pt exp x
  intro.x:R
derivable_pt exp x
  unfold derivable_pt.x:R
{l : R | derivable_pt_abs exp x l}
  exists (exp x).x:R
derivable_pt_abs exp x (exp x)
  apply derivable_pt_lim_exp.
Qed.

Lemma derivable_pt_cosh : forall x:R, derivable_pt cosh x.forall x : R, derivable_pt cosh x
Proof.forall x : R, derivable_pt cosh x
  intro.x:R
derivable_pt cosh x
  unfold derivable_pt.x:R
{l : R | derivable_pt_abs cosh x l}
  exists (sinh x).x:R
derivable_pt_abs cosh x (sinh x)
  apply derivable_pt_lim_cosh.
Qed.

Lemma derivable_pt_sinh : forall x:R, derivable_pt sinh x.forall x : R, derivable_pt sinh x
Proof.forall x : R, derivable_pt sinh x
  intro.x:R
derivable_pt sinh x
  unfold derivable_pt.x:R
{l : R | derivable_pt_abs sinh x l}
  exists (cosh x).x:R
derivable_pt_abs sinh x (cosh x)
  apply derivable_pt_lim_sinh.
Qed.

Lemma derivable_exp : derivable exp.derivable exp
Proof.derivable exp
  unfold derivable; apply derivable_pt_exp.
Qed.

Lemma derivable_cosh : derivable cosh.derivable cosh
Proof.derivable cosh
  unfold derivable; apply derivable_pt_cosh.
Qed.

Lemma derivable_sinh : derivable sinh.derivable sinh
Proof.derivable sinh
  unfold derivable; apply derivable_pt_sinh.
Qed.

Lemma derive_pt_exp :
  forall x:R, derive_pt exp x (derivable_pt_exp x) = exp x.forall x : R,
derive_pt exp x (derivable_pt_exp x) = exp x
Proof.forall x : R,
derive_pt exp x (derivable_pt_exp x) = exp x
  intro; apply derive_pt_eq_0.x:R
derivable_pt_lim exp x (exp x)
  apply derivable_pt_lim_exp.
Qed.

Lemma derive_pt_cosh :
  forall x:R, derive_pt cosh x (derivable_pt_cosh x) = sinh x.forall x : R,
derive_pt cosh x (derivable_pt_cosh x) = sinh x
Proof.forall x : R,
derive_pt cosh x (derivable_pt_cosh x) = sinh x
  intro; apply derive_pt_eq_0.x:R
derivable_pt_lim cosh x (sinh x)
  apply derivable_pt_lim_cosh.
Qed.

Lemma derive_pt_sinh :
  forall x:R, derive_pt sinh x (derivable_pt_sinh x) = cosh x.forall x : R,
derive_pt sinh x (derivable_pt_sinh x) = cosh x
Proof.forall x : R,
derive_pt sinh x (derivable_pt_sinh x) = cosh x
  intro; apply derive_pt_eq_0.x:R
derivable_pt_lim sinh x (cosh x)
  apply derivable_pt_lim_sinh.
Qed.

Lemma sinh_lt : forall x y, x < y -> sinh x < sinh y.forall x y : R, x < y -> sinh x < sinh y
intros x y xy; destruct (MVT_cor2 sinh cosh x y xy) as [c [Pc _]].x, y:R
xy:x < y
forall c : R,
x <= c <= y -> derivable_pt_lim sinh c (cosh c)
x, y:R
xy:x < y
c:R
Pc:sinh y - sinh x = cosh c * (y - x)
sinh x < sinh y
 intros; apply derivable_pt_lim_sinh.x, y:R
xy:x < y
c:R
Pc:sinh y - sinh x = cosh c * (y - x)
sinh x < sinh y
apply Rplus_lt_reg_l with (Ropp (sinh x)); rewrite Rplus_opp_l, Rplus_comm.x, y:R
xy:x < y
c:R
Pc:sinh y - sinh x = cosh c * (y - x)
0 < sinh y + - sinh x
unfold Rminus at 1 in Pc; rewrite Pc; apply Rmult_lt_0_compat;[ | ].x, y:R
xy:x < y
c:R
Pc:sinh y + - sinh x = cosh c * (y - x)
0 < cosh c
x, y:R
xy:x < y
c:R
Pc:sinh y + - sinh x = cosh c * (y - x)
0 < y - x
 unfold cosh; apply Rmult_lt_0_compat;[|apply Rinv_0_lt_compat, Rlt_0_2].x, y:R
xy:x < y
c:R
Pc:sinh y + - sinh x = cosh c * (y - x)
0 < exp c + exp (- c)
x, y:R
xy:x < y
c:R
Pc:sinh y + - sinh x = cosh c * (y - x)
0 < y - x
 now apply Rplus_lt_0_compat; apply exp_pos.x, y:R
xy:x < y
c:R
Pc:sinh y + - sinh x = cosh c * (y - x)
0 < y - x
now apply Rlt_Rminus; assumption.
Qed.