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

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

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

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

Require Import Reals Omega mathcomp.ssreflect.ssreflect.
Require Import Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries.
Require Import Lim_seq RInt_analysis.

(** This file describes basic properties (such as limits or
differentiability) about basic functions: absolute value, inverse,
square root, power, exponential and so on.*)

(** * Absolute value *)

(** ** in an [AbsRing] *)

Lemma continuous_abs {K : AbsRing} (x : K) :
  continuous abs x.
Proof.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  apply filterlim_locally => /= eps.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists eps => /= y Hy.
(* Goal: @ball R_UniformSpace (@abs K x) (pos eps) (@abs K y) *)
  eapply Rle_lt_trans, Hy.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  wlog: x y Hy / (abs x <= abs y) => [Hw | Hxy].
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    case: (Rle_lt_dec (abs x) (abs y)) => Hxy.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    by apply Hw.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    rewrite abs_minus (abs_minus y).
(* Goal: Rle (@abs R_AbsRing (@minus (AbsRing.AbelianGroup R_AbsRing) (@abs K x) (@abs K y))) (@abs K (@minus (AbsRing.AbelianGroup K) x y)) *)
(* Goal: Rle (@abs R_AbsRing (@minus (AbsRing.AbelianGroup R_AbsRing) (@abs K y) (@abs K x))) (@abs K (@minus (AbsRing.AbelianGroup K) y x)) *)
    apply Hw, Rlt_le, Hxy.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    by apply ball_sym.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite {1}/abs /=.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite Rabs_pos_eq.
(* Goal: Rle (@minus (AbsRing.AbelianGroup R_AbsRing) (@abs K y) (@abs K x)) (@abs K (@minus (AbsRing.AbelianGroup K) y x)) *)
(* Goal: Rle (IZR Z0) (@minus (AbsRing.AbelianGroup R_AbsRing) (@abs K y) (@abs K x)) *)
  apply Rle_minus_l.
(* Goal: Rle (@abs K y) (Rplus (@abs K (@minus (AbsRing.AbelianGroup K) y x)) (@abs K x)) *)
(* Goal: Rle (IZR Z0) (@minus (AbsRing.AbelianGroup R_AbsRing) (@abs K y) (@abs K x)) *)
  eapply Rle_trans, abs_triangle.
(* Goal: Rle (@abs K y) (@abs K (@plus (AbsRing.AbelianGroup K) (@minus (AbsRing.AbelianGroup K) y x) x)) *)
(* Goal: Rle (IZR Z0) (@minus (AbsRing.AbelianGroup R_AbsRing) (@abs K y) (@abs K x)) *)
  apply Req_le, f_equal.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by rewrite /minus -plus_assoc plus_opp_l plus_zero_r.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply -> Rminus_le_0.
Qed.
Lemma filterlim_abs_0 {K : AbsRing} :
  (forall x : K, abs x = 0 -> x = zero) ->
  filterlim (abs (K := K)) (locally' (zero (G := K))) (at_right 0).
Proof.
(* Goal: forall _ : forall (x : AbsRing.sort K) (_ : @eq R (@abs K x) (IZR Z0)), @eq (AbsRing.sort K) x (@zero (AbsRing.AbelianGroup K)), @filterlim (AbsRing.sort K) R (@abs K) (@locally' (AbsRing_UniformSpace K) (@zero (AbsRing.AbelianGroup K))) (at_right (IZR Z0)) *)
intros H P [eps HP].
(* Goal: @filtermap (AbsRing.sort K) R (@abs K) (@locally' (AbsRing_UniformSpace K) (@zero (AbsRing.AbelianGroup K))) P *)
exists eps.
(* Goal: forall (y : UniformSpace.sort (AbsRing_UniformSpace K)) (_ : @ball (AbsRing_UniformSpace K) (@zero (AbsRing.AbelianGroup K)) (pos eps) y) (_ : not (@eq (UniformSpace.sort (AbsRing_UniformSpace K)) y (@zero (AbsRing.AbelianGroup K)))), P (@abs K y) *)
intros x Hx Hx'.
(* Goal: P (@abs K x) *)
apply HP.
(* Goal: @ball R_UniformSpace (IZR Z0) (pos eps) (@abs K x) *)
(* Goal: Rlt (IZR Z0) (@abs K x) *)
revert Hx.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
rewrite /ball /= /AbsRing_ball !minus_zero_r {2}/abs /= Rabs_pos_eq.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
by [].
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
by apply abs_ge_0.
(* Goal: Rlt (IZR Z0) (@abs K x) *)
assert (abs x <> 0).
(* Goal: not (@eq R (@abs K x) (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (@abs K x) *)
contradict Hx' ; by apply H.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
case: (abs_ge_0 x) => // H1.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
by rewrite -H1 in H0.
Qed.

(** ** in [R] *)

Lemma continuous_Rabs (x : R) :
  continuous Rabs x.
Proof.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply @continuous_abs.
Qed.

Lemma filterlim_Rabs (x : Rbar) :
  filterlim Rabs (Rbar_locally' x) (Rbar_locally (Rbar_abs x)).
Proof.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  destruct x as [x| | ] => //=.

  eapply filterlim_filter_le_1, continuous_Rabs.
  intros P [d HP] ; exists d => y Hy _.
(* Goal: P (@abs K x) *)
  by apply HP.

  eapply filterlim_ext_loc.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists 0 => y Hy.
  rewrite Rabs_pos_eq // ; by apply Rlt_le.
  apply is_lim_id.

  eapply filterlim_ext_loc.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists 0 => y Hy.
  rewrite -Rabs_Ropp Rabs_pos_eq // -Ropp_0 ;
  by apply Ropp_le_contravar, Rlt_le.
  apply (is_lim_opp id m_infty m_infty), is_lim_id.
Qed.
Lemma is_lim_Rabs (f : R -> R) (x l : Rbar) :
  is_lim f x l -> is_lim (fun x => Rabs (f x)) x (Rbar_abs l).
Proof.
  destruct l as [l| | ] ; simpl ; intros ; first last.
  eapply is_lim_comp.
  2: by apply H.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply filterlim_Rabs.
  destruct x ; by exists (mkposreal _ Rlt_0_1).
  eapply is_lim_comp.
  2: by apply H.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply filterlim_Rabs.
  destruct x ; by exists (mkposreal _ Rlt_0_1).
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  apply is_lim_comp_continuous => //.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply continuous_Rabs.
Qed.

Lemma filterlim_Rabs_0 :
  filterlim Rabs (Rbar_locally' 0) (at_right 0).
Proof.
(* Goal: @filterlim R R Rabs (Rbar_locally' (Finite (IZR Z0))) (at_right (IZR Z0)) *)
  apply @filterlim_abs_0.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rabs_eq_0.
Qed.
Lemma is_lim_Rabs_0 (f : R -> R) (x : Rbar) :
  is_lim f x 0 -> Rbar_locally' x (fun x => f x <> 0)
    -> filterlim (fun x => Rabs (f x)) (Rbar_locally' x) (at_right 0).
Proof.
(* Goal: forall (i p : nat) (x : R) (_ : lt p i), @eq R (Derive_n (fun x0 : R => pow x0 p) i x) (IZR Z0) *)
  intros.
(* Goal: @filterlim R R (fun x : R => Rabs (f x)) (Rbar_locally' x) (at_right (IZR Z0)) *)
  eapply filterlim_comp, filterlim_Rabs_0.
(* Goal: @filterlim R R f (Rbar_locally' x) (at_left (IZR Z0)) *)
  intros P HP.
(* Goal: @filtermap R R f (Rbar_locally' x) P *)
  apply H in HP.
(* Goal: @filtermap R R f (Rbar_locally' x) P *)
  generalize (filter_and _ _ H0 HP).
(* Goal: forall _ : Rbar_locally' x (fun x : R => and (not (@eq R (f x) (IZR Z0))) (forall _ : not (@eq (UniformSpace.sort R_UniformSpace) (f x) (IZR Z0)), P (f x))), @filtermap R R f (Rbar_locally' x) P *)
  rewrite /filtermap /= ; apply filter_imp.
(* Goal: forall (x : R) (_ : and (not (@eq R (f x) (IZR Z0))) (forall _ : not (@eq R (f x) (IZR Z0)), P (f x))), P (f x) *)
  intros y Hy.
(* Goal: P (f y) *)
  apply Hy, Hy.
Qed.

Lemma filterdiff_Rabs (x : R) :
  x <> 0 -> filterdiff Rabs (locally x) (fun y : R => scal y (sign x)).
Proof.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -/(is_derive Rabs x (sign x)).
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
  move => Hx0.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: (Rle_lt_dec 0 x) => Hx.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: Hx => //= Hx.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite sign_eq_1 //.
  eapply is_derive_ext_loc.
  apply locally_interval with 0 p_infty.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by [].
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by [].
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
  move => /= y Hy _.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite Rabs_pos_eq //.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rlt_le.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply @is_derive_id.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply sym_eq in Hx.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite sign_eq_m1 //.
  eapply is_derive_ext_loc.
  apply locally_interval with m_infty 0.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by [].
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by [].
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
  move => /= y _ Hy.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -Rabs_Ropp Rabs_pos_eq //.
  rewrite -Ropp_0 ; by apply Rlt_le, Ropp_lt_contravar.
  apply @is_derive_opp.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply @is_derive_id.
Qed.
Lemma is_derive_Rabs (f : R -> R) (x df : R) :
  is_derive f x df -> f x <> 0
    -> is_derive (fun x => Rabs (f x)) x (sign (f x) * df).
Proof.
  intros Hf Hfx.
  evar_last.
  apply is_derive_comp, Hf.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply filterdiff_Rabs.
(* Goal: @eq R (Rdiv (Rmult x (pow x n)) (INR (Init.Nat.add (fact n) (Init.Nat.mul n (fact n))))) (Rmult (Rinv (INR (Init.Nat.add (fact n) (Init.Nat.mul n (fact n))))) (Rmult x (pow x n))) *)
(* Goal: Rle (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n (S N))) *)
  apply Rmult_comm.
Qed.

(** * Inverse function *)

Lemma filterlim_Rinv_0_right :
  filterlim Rinv (at_right 0) (Rbar_locally p_infty).
Proof.
(* Goal: @filterlim R R ln (at_right (IZR Z0)) (Rbar_locally m_infty) *)
  intros P [M HM].
(* Goal: @filtermap R R Rinv (at_right (IZR Z0)) P *)
  have Hd : 0 < / Rmax 1 M.
(* Goal: Rlt (IZR Z0) (Rinv (Rmax (IZR (Zpos xH)) M)) *)
(* Goal: @filtermap R R Rinv (at_right (IZR Z0)) P *)
    apply Rinv_0_lt_compat.
(* Goal: Rlt (IZR Z0) (Rmax (IZR (Zpos xH)) M) *)
(* Goal: @filtermap R R Rinv (at_right (IZR Z0)) P *)
    apply Rlt_le_trans with (2 := Rmax_l _ _).
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    by apply Rlt_0_1.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists (mkposreal _ Hd) => x /= Hx Hx0.
(* Goal: P (ln x) *)
  apply HM.
(* Goal: Rlt M (Rinv x) *)
  apply Rle_lt_trans with (1 := Rmax_r 1 M).
  replace (Rmax 1 M) with (/ / Rmax 1 M)
  by (field ; apply Rgt_not_eq, Rlt_le_trans with (2 := Rmax_l _ _), Rlt_0_1).
(* Goal: Rlt (Rinv (Rinv (Rmax (IZR (Zpos xH)) M))) (Rinv x) *)
  apply Rinv_lt_contravar.
(* Goal: Rlt (IZR Z0) (Rmult x (Rinv (Rmax (IZR (Zpos xH)) M))) *)
(* Goal: Rlt x (Rinv (Rmax (IZR (Zpos xH)) M)) *)
  apply Rdiv_lt_0_compat with (1 := Hx0).
(* Goal: Rlt (IZR Z0) (Rmax (IZR (Zpos xH)) M) *)
(* Goal: Rlt x (Rinv (Rmax (IZR (Zpos xH)) M)) *)
  apply Rlt_le_trans with (2 := Rmax_l _ _), Rlt_0_1.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /ball /= /AbsRing_ball /= /abs /minus /plus /opp /= in Hx.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -/(Rminus _ _) Rminus_0_r Rabs_pos_eq // in Hx.
(* Goal: Rle (IZR Z0) x *)
  exact: Rlt_le.
Qed.
Lemma is_lim_Rinv_0_right (f : R -> R) (x : Rbar) :
  is_lim f x 0 -> Rbar_locally' x (fun x => 0 < f x) ->
  is_lim (fun x => / (f x)) x p_infty.
Proof.
(* Goal: forall (i p : nat) (x : R) (_ : lt p i), @eq R (Derive_n (fun x0 : R => pow x0 p) i x) (IZR Z0) *)
  intros.
(* Goal: is_lim (fun x : R => Rinv (f x)) x p_infty *)
  eapply filterlim_comp, filterlim_Rinv_0_right.
(* Goal: @filterlim R R f (Rbar_locally' x) (at_left (IZR Z0)) *)
  intros P HP.
(* Goal: @filtermap R R f (Rbar_locally' x) P *)
  apply H in HP.
(* Goal: @filtermap R R f (Rbar_locally' x) P *)
  generalize (filter_and _ _ H0 HP).
  rewrite /filtermap ;
  apply filter_imp => y Hy.
(* Goal: P (f y) *)
  by apply Hy, Hy.
Qed.

Lemma filterlim_Rinv_0_left :
  filterlim Rinv (at_left 0) (Rbar_locally m_infty).
Proof.
  eapply filterlim_ext_loc.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists (mkposreal _ Rlt_0_1) => /= y _ Hy0.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -{2}(Ropp_involutive y).
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -Ropp_inv_permute.
  reflexivity.
  contradict Hy0.
  apply Rle_not_lt, Req_le.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by rewrite -(Ropp_involutive y) Hy0 Ropp_0.
  eapply filterlim_comp.
  eapply filterlim_comp.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply filterlim_Ropp_left.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite Ropp_0.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply filterlim_Rinv_0_right.
  apply filterlim_Rbar_opp.
Qed.
Lemma is_lim_Rinv_0_left (f : R -> R) (x : Rbar) :
  is_lim f x 0 -> Rbar_locally' x (fun x => f x < 0) ->
  is_lim (fun x => / (f x)) x m_infty.
Proof.
(* Goal: forall (i p : nat) (x : R) (_ : lt p i), @eq R (Derive_n (fun x0 : R => pow x0 p) i x) (IZR Z0) *)
  intros.
(* Goal: is_lim (fun x : R => Rinv (f x)) x m_infty *)
  eapply filterlim_comp, filterlim_Rinv_0_left.
(* Goal: @filterlim R R f (Rbar_locally' x) (at_left (IZR Z0)) *)
  intros P HP.
(* Goal: @filtermap R R f (Rbar_locally' x) P *)
  apply H in HP.
(* Goal: @filtermap R R f (Rbar_locally' x) P *)
  generalize (filter_and _ _ H0 HP).
  rewrite /filtermap ;
  apply filter_imp => y Hy.
(* Goal: P (f y) *)
  by apply Hy, Hy.
Qed.

(** * Square root function *)

Lemma filterlim_sqrt_p : filterlim sqrt (Rbar_locally' p_infty) (Rbar_locally p_infty).
Proof.
(* Goal: is_lim (fun x : R => Rdiv (sin x) x) (Finite (IZR Z0)) (Finite (IZR (Zpos xH))) *)
  apply is_lim_spec.
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
  move => M.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists ((Rmax 0 M)²) => x Hx.
(* Goal: Rlt M (sqrt x) *)
  apply Rle_lt_trans with (1 := Rmax_r 0 M).
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -(sqrt_Rsqr (Rmax 0 M)).
(* Goal: Rlt (sqrt (Rsqr (Rmax (IZR Z0) M))) (sqrt x) *)
(* Goal: Rle (IZR Z0) (Rmax (IZR Z0) M) *)
  apply sqrt_lt_1_alt.
(* Goal: and (Rle (IZR Z0) (Rsqr (Rmax (IZR Z0) M))) (Rlt (Rsqr (Rmax (IZR Z0) M)) x) *)
(* Goal: Rle (IZR Z0) (Rmax (IZR Z0) M) *)
  split.
(* Goal: Rle (IZR Z0) (Rsqr (Rmax (IZR Z0) M)) *)
(* Goal: Rlt (Rsqr (Rmax (IZR Z0) M)) x *)
(* Goal: Rle (IZR Z0) (Rmax (IZR Z0) M) *)
  apply Rle_0_sqr.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Hx.
(* Goal: Rle (IZR Z0) (Rmax (IZR Z0) M) *)
  apply Rmax_l.
Qed.
Lemma is_lim_sqrt_p (f : R -> R) (x : Rbar) :
  is_lim f x p_infty
  -> is_lim (fun x => sqrt (f x)) x p_infty.
Proof.
(* Goal: forall (i p : nat) (x : R) (_ : lt p i), @eq R (Derive_n (fun x0 : R => pow x0 p) i x) (IZR Z0) *)
  intros.
(* Goal: is_lim (fun x : R => sqrt (f x)) x p_infty *)
  eapply filterlim_comp, filterlim_sqrt_p.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply H.
Qed.

Lemma filterdiff_sqrt (x : R) :
  0 < x -> filterdiff sqrt (locally x) (fun y => scal y (/ (2 * sqrt x))).
Proof.
(* Goal: forall _ : Rlt (IZR Z0) x, @filterdiff R_AbsRing R_NormedModule R_NormedModule sqrt (@locally R_UniformSpace x) (fun y : NormedModule.sort R_AbsRing R_NormedModule => @scal R_Ring R_ModuleSpace y (Rinv (Rmult (IZR (Zpos (xO xH))) (sqrt x)))) *)
  intros Hx.
(* Goal: @filterdiff R_AbsRing R_NormedModule R_NormedModule sqrt (@locally R_UniformSpace x) (fun y : NormedModule.sort R_AbsRing R_NormedModule => @scal R_Ring R_ModuleSpace y (Rinv (Rmult (IZR (Zpos (xO xH))) (sqrt x)))) *)
  apply is_derive_Reals.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply derivable_pt_lim_sqrt.
Qed.
Lemma is_derive_sqrt (f : R -> R) (x df : R) :
  is_derive f x df -> 0 < f x
  -> is_derive (fun x => sqrt (f x)) x (df / (2 * sqrt (f x))).
Proof.
  intros Hf Hfx.
  evar_last.
  eapply is_derive_comp.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply filterdiff_sqrt.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Hf.
  reflexivity.
Qed.

(** * Power function *)
Section nat_to_ring.

Context {K : Ring}.

Definition nat_to_ring (n : nat) : K :=
  sum_n_m (fun _ => one) 1 n.
Lemma nat_to_ring_O :
  nat_to_ring O = zero.
Proof.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /nat_to_ring sum_n_m_zero //.
Qed.
Lemma nat_to_ring_Sn (n : nat) :
  nat_to_ring (S n) = plus (nat_to_ring n) one.
Proof.
(* Goal: @eq (Ring.sort K) (nat_to_ring (S n)) (@plus (Ring.AbelianGroup K) (nat_to_ring n) (@one K)) *)
  case: n => [ | n] ; rewrite /nat_to_ring.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite sum_n_n sum_n_m_zero //.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by rewrite plus_zero_l.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite sum_n_Sm //.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply le_n_S, le_O_n.
Qed.

End nat_to_ring.

Section is_derive_mult.

Context {K : AbsRing}.

Lemma is_derive_mult (f g : K -> K) x (df dg : K) :
  is_derive f x df -> is_derive g x dg
  -> (forall n m : K, mult n m = mult m n)
  -> is_derive (fun x : K => mult (f x) (g x)) x (plus (mult df (g x)) (mult (f x) dg)).
Proof.
  intros Hf Hg Hmult.
  eapply filterdiff_ext_lin.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  eapply filterdiff_comp_2 => /=.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Hf.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Hg.
  eapply filterdiff_ext_lin.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  apply (filterdiff_mult (f x,g x)) => /=.
  intros P [d Hd].
  assert (Cf := ex_derive_continuous f x).
  assert (Cg := ex_derive_continuous g x).
  destruct (fun H => proj1 (filterlim_locally _ _) (Cf H) d) as [d1 Hd1].
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    eexists ; by apply Hf.
  destruct (fun H => proj1 (filterlim_locally _ _) (Cg H) d) as [d2 Hd2].
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    eexists ; by apply Hg.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists (mkposreal _ (Rmin_stable_in_posreal d1 d2)) => /= y Hy.
  apply Hd ; split => /=.
  eapply (Hd1 y), ball_le, Hy.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rmin_l.
  eapply (Hd2 y), ball_le, Hy.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rmin_r.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Hmult.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  simpl => [[y1 y2]] /=.
  reflexivity.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  simpl => y.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /scal /=.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite mult_assoc (Hmult (f x)) -!mult_assoc.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by rewrite mult_distr_l.
Qed.

End is_derive_mult.

Lemma filterdiff_pow_n {K : AbsRing} (x : K) (n : nat) :
  (forall a b : K, mult a b = mult b a)
  -> filterdiff (fun y : K => pow_n y n) (locally x)
    (fun y : K => scal y (mult (nat_to_ring n) (pow_n x (pred n)))).
Proof.
  intros Hmult.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -/(is_derive (fun y : K => pow_n y n) x (mult (nat_to_ring n) (pow_n x (pred n)))).
(* Goal: @eq R (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) n) *)
(* Goal: Rle (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n (S N))) *)
  elim: n => [ | n IH] /=.
  evar_last.
  apply is_derive_const.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by rewrite nat_to_ring_O mult_zero_l.
  evar_last.
  eapply is_derive_mult.
  apply is_derive_id.
  apply IH.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Hmult.
  simpl.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite nat_to_ring_Sn mult_one_l mult_assoc (Hmult x) -mult_assoc.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite mult_distr_r mult_one_l plus_comm.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  apply f_equal2 => //.
  clear ; case: n => [ | n] //=.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by rewrite nat_to_ring_O !mult_zero_l.
Qed.

Lemma is_derive_n_pow_smalli: forall i p x, (i <= p)%nat ->
  is_derive_n (fun x : R => x ^ p) i x
    (INR (fact p) / INR (fact (p - i)%nat) * x ^ (p - i)%nat).
Proof.
(* Goal: @eq R (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) n) *)
(* Goal: Rle (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n (S N))) *)
  elim => /= [ | i IH] p x Hip.
  rewrite -minus_n_O ; field.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply INR_fact_neq_0.
  eapply is_derive_ext.
  intros t.
  apply sym_equal, is_derive_n_unique, IH.
  eapply le_trans, Hip ; by apply le_n_Sn.
  evar_last.
  apply is_derive_scal, is_derive_pow, is_derive_id.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite MyNat.sub_succ_r.
  change one with 1.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite {1 2} (S_pred (p - i) O) /fact -/fact ?mult_INR.
  field.
(* Goal: and (Rle (IZR Z0) (Rsqr (Rmax (IZR Z0) M))) (Rlt (Rsqr (Rmax (IZR Z0) M)) x) *)
(* Goal: Rle (IZR Z0) (Rmax (IZR Z0) M) *)
  split.
  apply INR_fact_neq_0.
  apply not_0_INR, sym_not_eq, O_S.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply lt_minus_O_lt.
Qed.
Lemma Derive_n_pow_smalli: forall i p x, (i <= p)%nat ->
  Derive_n (fun x : R => x ^ p) i x
    = INR (fact p) / INR (fact (p - i)%nat) * x ^ (p - i)%nat.
Proof.
(* Goal: forall (i p : nat) (x : R) (_ : lt p i), @eq R (Derive_n (fun x0 : R => pow x0 p) i x) (IZR Z0) *)
  intros.
(* Goal: @eq R (Derive_n (fun x : R => pow x p) i x) (Rmult (Rdiv (INR (fact p)) (INR (fact (Init.Nat.sub p i)))) (pow x (Init.Nat.sub p i))) *)
  now apply is_derive_n_unique, is_derive_n_pow_smalli.
Qed.
Lemma is_derive_n_pow_bigi: forall i p x,  (p < i) %nat ->
                         is_derive_n (fun x : R => x ^ p) i x 0.
Proof.
  elim => /=  [ | i IH] p x Hip.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply lt_n_O in Hip.
  apply lt_n_Sm_le, le_lt_eq_dec in Hip.
  case: Hip => [Hip | ->] ;
  eapply is_derive_ext.
  intros t ; by apply sym_equal, is_derive_n_unique, IH.
  apply @is_derive_const.
  intros t ; rewrite Derive_n_pow_smalli.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by rewrite minus_diag /=.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply le_refl.
  by apply @is_derive_const.
Qed.
Lemma Derive_n_pow_bigi: forall i p x,  (p < i) %nat ->
                         Derive_n (fun x : R => x ^ p) i x = 0.
Proof.
(* Goal: forall (i p : nat) (x : R) (_ : lt p i), @eq R (Derive_n (fun x0 : R => pow x0 p) i x) (IZR Z0) *)
  intros.
(* Goal: @eq R (Derive_n (fun x : R => pow x p) i x) (IZR Z0) *)
  now apply is_derive_n_unique, is_derive_n_pow_bigi.
Qed.

Lemma Derive_n_pow i p x:
  Derive_n (fun x : R => x ^ p) i x =
    match (le_dec i p) with
    | left _ => INR (fact p) / INR (fact (p -i)%nat) * x ^ (p - i)%nat
    | right _ => 0
    end.
Proof.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
case: le_dec => H.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
by apply Derive_n_pow_smalli.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
by apply Derive_n_pow_bigi, not_le.
Qed.

Lemma ex_derive_n_pow i p x: ex_derive_n (fun x : R => x ^ p) i x.
Proof.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: i => //= i.
(* Goal: @ex_derive R_AbsRing R_NormedModule (Derive_n (fun x : R => pow x p) i) x *)
  exists (Derive_n (fun x : R => x ^ p) (S i) x).
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite Derive_n_pow.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: le_dec => Hip.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply (is_derive_n_pow_smalli (S i)).
(* Goal: @is_derive R_AbsRing R_NormedModule (Derive_n (fun x : R => pow x p) i) x (IZR Z0) *)
  apply (is_derive_n_pow_bigi (S i)) ; omega.
Qed.

Lemma is_RInt_pow :
  forall a b n,
  is_RInt (fun x => pow x n) a b (pow b (S n) / INR (S n) - pow a (S n) / INR (S n)).
Proof.
intros a b n.
set f := fun x => pow x (S n) / INR (S n).
fold (f a) (f b).
assert (H: forall x : R, is_derive f x (pow x n)).
  intros x.
  evar_last.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /f /Rdiv -[Rmult]/(scal (V := R_NormedModule)).
  apply is_derive_scal_l.
  apply is_derive_pow, is_derive_id.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /pred.
  set k := INR (S n).
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /scal /= /mult /one /=.
  field.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /k S_INR.
  apply Rgt_not_eq, INRp1_pos.
  apply: is_RInt_derive => x Hx //.
apply continuity_pt_filterlim.
apply derivable_continuous_pt.
apply derivable_pt_pow.
Qed.

(** * Exponential function *)

Lemma exp_ge_taylor (x : R) (n : nat) :
  0 <= x -> sum_f_R0 (fun k => x^k / INR (fact k)) n <= exp x.
Proof.
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
  move => Hx.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /exp /exist_exp.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: Alembert_C3 => /= y Hy.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  apply Rnot_lt_le => H.
(* Goal: False *)
  apply Rminus_lt_0 in H.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: (Hy _ H) => N {Hy} Hy.
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
  move: (Hy _ (le_plus_r n N)) => {Hy}.
(* Goal: forall _ : Rlt (R_dist (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n N)) y) (Rminus (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) y), False *)
  apply Rle_not_lt.
(* Goal: Rle (Rminus (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) y) (R_dist (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n N)) y) *)
  apply Rle_trans with (2 := Rle_abs _).
(* Goal: Rle (Rminus (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) y) (Rminus (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n N)) y) *)
  apply Rplus_le_compat_r.
(* Goal: @eq R (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) n) *)
(* Goal: Rle (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n (S N))) *)
  elim: N => [ | N IH].
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite plus_0_r.
(* Goal: Rle (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) n) *)
(* Goal: Rle (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n (S N))) *)
  apply Req_le.
(* Goal: @eq R (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) n) *)
(* Goal: Rle (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n (S N))) *)
  elim: (n) => {n H} [ | n /= <-].
(* Goal: @eq R (Rdiv (Rmult x (pow x n)) (INR (Init.Nat.add (fact n) (Init.Nat.mul n (fact n))))) (Rmult (Rinv (INR (Init.Nat.add (fact n) (Init.Nat.mul n (fact n))))) (Rmult x (pow x n))) *)
(* Goal: Rle (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n (S N))) *)
  apply Rmult_comm.
(* Goal: @eq R (Rplus (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (Rdiv (Rmult x (pow x n)) (INR (Init.Nat.add (fact n) (Init.Nat.mul n (fact n)))))) (Rplus (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (Rmult (Rinv (INR (Init.Nat.add (fact n) (Init.Nat.mul n (fact n))))) (Rmult x (pow x n)))) *)
(* Goal: Rle (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n (S N))) *)
  apply f_equal.
(* Goal: @eq R (Rdiv (Rmult x (pow x n)) (INR (Init.Nat.add (fact n) (Init.Nat.mul n (fact n))))) (Rmult (Rinv (INR (Init.Nat.add (fact n) (Init.Nat.mul n (fact n))))) (Rmult x (pow x n))) *)
(* Goal: Rle (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n (S N))) *)
  apply Rmult_comm.
(* Goal: Rle (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n (S N))) *)
  apply Rle_trans with (1 := IH).
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -plus_n_Sm.
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
  move: (n + N)%nat => {n H N IH} n.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /sum_f_R0 -/sum_f_R0.
(* Goal: Rle (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) n) (Rplus (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) n) (Rmult (Rinv (INR (fact (S n)))) (pow x (S n)))) *)
  apply Rminus_le_0 ; ring_simplify.
(* Goal: Rle (IZR Z0) (Rmult (Rinv (INR (fact (S n)))) (pow x (S n))) *)
  apply Rmult_le_pos.
(* Goal: Rle (IZR Z0) (Rinv (INR (fact (S n)))) *)
(* Goal: Rle (IZR Z0) (pow x (S n)) *)
  apply Rlt_le, Rinv_0_lt_compat, INR_fact_lt_0.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply pow_le.
Qed.

(** Definition *)

Lemma is_exp_Reals (x : R) :
  is_pseries (fun n => / INR (fact n)) x (exp x).
Proof.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /exp.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: exist_exp => l /= Hl.
(* Goal: @is_pseries R_AbsRing R_NormedModule (fun n : nat => Rinv (INR (fact n))) x l *)
  apply Series.is_series_Reals in Hl.
  move: Hl ;
  apply Series.is_series_ext => n.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by rewrite Rmult_comm pow_n_pow.
Qed.
Lemma exp_Reals (x : R) :
  exp x = PSeries (fun n => / INR (fact n)) x.
Proof.
(* Goal: @eq R (exp x) (PSeries (fun n : nat => Rinv (INR (fact n))) x) *)
  apply sym_eq, is_pseries_unique.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply is_exp_Reals.
Qed.

(** Limits *)

Lemma is_lim_exp_p : is_lim (fun y => exp y) p_infty p_infty.
Proof.
  apply is_lim_le_p_loc with (fun y => 1 + y).
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists 0 => y Hy.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rlt_le, exp_ineq1.
  pattern p_infty at 2.
  replace p_infty with (Rbar_plus 1 p_infty) by auto.
  eapply is_lim_plus.
  apply is_lim_const.
  apply is_lim_id.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by [].
Qed.
Lemma is_lim_exp_m : is_lim (fun y => exp y) m_infty 0.
Proof.
  evar_last.
  apply is_lim_ext with (fun y => /(exp (- y))).
  move => y ; rewrite exp_Ropp ; apply Rinv_involutive.
  apply Rgt_not_eq, exp_pos.
  apply is_lim_inv.
  apply is_lim_comp with p_infty.
  apply is_lim_exp_p.
  replace p_infty with (Rbar_opp m_infty) by auto.
  apply is_lim_opp.
  apply is_lim_id.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply filter_forall.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by [].
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by [].
Qed.

Lemma ex_lim_exp (x : Rbar) : ex_lim (fun y => exp y) x.
Proof.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: x => [x | | ].
(* Goal: ex_lim (fun y : R => exp y) (Finite x) *)
(* Goal: ex_lim (fun y : R => exp y) p_infty *)
(* Goal: ex_lim (fun y : R => exp y) m_infty *)
  apply ex_finite_lim_correct, ex_lim_continuity.
(* Goal: continuity_pt (fun y : R => exp y) x *)
(* Goal: is_lim (fun y : R => exp y) p_infty p_infty *)
(* Goal: is_lim (fun y : R => exp y) m_infty (Finite (IZR Z0)) *)
  apply derivable_continuous_pt, derivable_pt_exp.
  exists p_infty ; by apply is_lim_exp_p.
(* Goal: ex_lim (fun y : R => exp y) m_infty *)
  exists 0 ; by apply is_lim_exp_m.
Qed.
Lemma Lim_exp (x : Rbar) :
  Lim (fun y => exp y) x =
    match x with
      | Finite x => exp x
      | p_infty => p_infty
      | m_infty => 0
    end.
Proof.
(* Goal: @eq Rbar (Lim (fun y : R => exp y) x) match x with | Finite x => Finite (exp x) | p_infty => p_infty | m_infty => Finite (IZR Z0) end *)
  apply is_lim_unique.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: x => [x | | ].
(* Goal: is_lim (fun y : R => exp y) (Finite x) (Finite (exp x)) *)
(* Goal: is_lim (fun y : R => exp y) p_infty p_infty *)
(* Goal: is_lim (fun y : R => exp y) m_infty (Finite (IZR Z0)) *)
  apply is_lim_continuity.
(* Goal: continuity_pt (fun y : R => exp y) x *)
(* Goal: is_lim (fun y : R => exp y) p_infty p_infty *)
(* Goal: is_lim (fun y : R => exp y) m_infty (Finite (IZR Z0)) *)
  apply derivable_continuous_pt, derivable_pt_exp.
  by apply is_lim_exp_p.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply is_lim_exp_m.
Qed.

Lemma is_lim_div_exp_p : is_lim (fun y => exp y / y) p_infty p_infty.
Proof.
  apply is_lim_le_p_loc with (fun y => (1 + y + y^2 / 2)/y).
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists 0 => y Hy.
  apply Rmult_le_compat_r.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rlt_le, Rinv_0_lt_compat.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /exp.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /exist_exp.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: Alembert_C3 => /= x Hx.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /Pser /infinite_sum in Hx.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  apply Rnot_lt_le => H.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: (Hx _ (proj1 (Rminus_lt_0 _ _) H)) => N {Hx} Hx.
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
  move: (Hx _ (le_plus_r 2 N)) => {Hx}.
(* Goal: forall _ : Rlt (R_dist (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n N)) y) (Rminus (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) y), False *)
  apply Rle_not_lt.
(* Goal: Rle (Rminus (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) y) (R_dist (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n N)) y) *)
  apply Rle_trans with (2 := Rle_abs _).
(* Goal: Rle (Rminus (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) y) (Rminus (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n N)) y) *)
  apply Rplus_le_compat_r.
(* Goal: @eq R (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) n) *)
(* Goal: Rle (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n (S N))) *)
  elim: N => [ | n IH].
  simpl ; apply Req_le ; field.
(* Goal: Rle (sum_f_R0 (fun k : nat => Rdiv (pow x k) (INR (fact k))) n) (sum_f_R0 (fun n : nat => Rmult (Rinv (INR (fact n))) (pow x n)) (Init.Nat.add n (S N))) *)
  apply Rle_trans with (1 := IH).
  rewrite -plus_n_Sm ; move: (2 + n)%nat => {n IH} n.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /sum_f_R0 -/sum_f_R0.
  rewrite Rplus_comm ; apply Rle_minus_l ; rewrite Rminus_eq_0.
(* Goal: Rle (IZR Z0) (Rmult (Rinv (INR (fact (S n)))) (pow x (S n))) *)
  apply Rmult_le_pos.
(* Goal: Rle (IZR Z0) (Rinv (INR (fact (S n)))) *)
(* Goal: Rle (IZR Z0) (pow x (S n)) *)
  apply Rlt_le, Rinv_0_lt_compat, INR_fact_lt_0.
  apply pow_le.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rlt_le.
  apply is_lim_ext_loc with (fun y => /y + 1 + y / 2).
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists 0 => y Hy.
  field.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rgt_not_eq.
  eapply is_lim_plus.
  eapply is_lim_plus.
  apply is_lim_inv.
  apply is_lim_id.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by [].
  apply is_lim_const.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by [].
  apply is_lim_div.
  apply is_lim_id.
  apply is_lim_const.
  apply Rbar_finite_neq, Rgt_not_eq, Rlt_0_2.
  simpl.
  apply Rgt_not_eq, Rinv_0_lt_compat, Rlt_0_2.
  simpl.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: Rle_dec (Rlt_le _ _ (Rinv_0_lt_compat 2 (Rlt_0_2))) => //= H _.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: Rle_lt_or_eq_dec (Rlt_not_eq _ _ (Rinv_0_lt_compat 2 (Rlt_0_2))) => //= H _.
Qed.

Lemma is_lim_mul_exp_m : is_lim (fun y => y * exp y) m_infty 0.
Proof.
  evar_last.
  apply is_lim_ext_loc with (fun y => - / (exp (-y) / (- y))).
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists 0 => y Hy.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite exp_Ropp.
  field.
(* Goal: and (Rle (IZR Z0) (Rsqr (Rmax (IZR Z0) M))) (Rlt (Rsqr (Rmax (IZR Z0) M)) x) *)
(* Goal: Rle (IZR Z0) (Rmax (IZR Z0) M) *)
  split.
  apply Rgt_not_eq, exp_pos.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rlt_not_eq.
  apply is_lim_opp.
  apply is_lim_inv.
  apply (is_lim_comp (fun y => exp y / y)) with p_infty.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply is_lim_div_exp_p.
  evar_last.
  apply is_lim_opp.
  apply is_lim_id.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by [].
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply filter_forall.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by [].
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  simpl ; by rewrite Ropp_0.
Qed.

Lemma is_lim_div_expm1_0 : is_lim (fun y => (exp y - 1) / y) 0 1.
Proof.
(* Goal: is_lim (fun x : R => Rdiv (sin x) x) (Finite (IZR Z0)) (Finite (IZR (Zpos xH))) *)
  apply is_lim_spec.
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
  move => eps.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: (derivable_pt_lim_exp_0 eps (cond_pos eps)) => delta H.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists delta => y Hy Hy0.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /= in Hy.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -/(Rminus _ _) Rminus_0_r in Hy.
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
  move: (H y Hy0 Hy).
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by rewrite Rplus_0_l exp_0.
Qed.

(** Integral *)

Lemma is_RInt_exp :
  forall a b,
  is_RInt exp a b (exp b - exp a).
Proof.
intros a b.
apply: is_RInt_derive.
  intros x _.
  apply is_derive_Reals, derivable_pt_lim_exp.
intros x _.
apply continuity_pt_filterlim.
apply derivable_continuous_pt.
apply derivable_pt_exp.
Qed.

(** * Natural logarithm *)

Lemma is_lim_ln_p : is_lim (fun y => ln y) p_infty p_infty.
Proof.
(* Goal: is_lim (fun x : R => Rdiv (sin x) x) (Finite (IZR Z0)) (Finite (IZR (Zpos xH))) *)
  apply is_lim_spec.
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
  move => M.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists (exp M) => x Hx.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -(ln_exp M).
(* Goal: Rlt (ln x) (ln (exp M)) *)
  apply ln_increasing.
(* Goal: Rlt (IZR Z0) (exp M) *)
(* Goal: Rlt (exp M) x *)
  apply exp_pos.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Hx.
Qed.

Lemma is_lim_ln_0 :
  filterlim ln (at_right 0) (Rbar_locally m_infty).
Proof.
(* Goal: @filterlim R R ln (at_right (IZR Z0)) (Rbar_locally m_infty) *)
intros P [M HM].
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
exists (mkposreal (exp M) (exp_pos _)) => x /= Hx Hx0.
(* Goal: P (ln x) *)
apply HM.
(* Goal: Rlt (ln x) M *)
rewrite <- (ln_exp M).
(* Goal: Rlt (ln x) (ln (exp M)) *)
apply ln_increasing.
(* Goal: Rlt (IZR Z0) x *)
(* Goal: Rlt x (exp M) *)
exact Hx0.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
rewrite /ball /= /AbsRing_ball /= /abs /minus /plus /opp /= in Hx.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
rewrite -/(Rminus _ _) Rminus_0_r Rabs_pos_eq in Hx.
(* Goal: Rlt x (exp M) *)
(* Goal: Rle (IZR Z0) x *)
exact Hx.
(* Goal: Rle (IZR Z0) x *)
now apply Rlt_le.
Qed.

Lemma is_lim_div_ln_p : is_lim (fun y => ln y / y) p_infty 0.
Proof.
(* Goal: @filtermap R R Rinv (at_right (IZR Z0)) P *)
  have H : forall x, 0 < x -> ln x < x.
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
    move => x Hx.
    apply Rminus_lt_0.
    apply Rlt_le_trans with (1 := Rlt_0_1).
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    case: (MVT_gen (fun y => y - ln y) 1 x (fun y => (y-1)/y)).
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
      move => z Hz.
      evar (l : R).
      replace ((z - 1) / z) with l.
(* Goal: @filterdiff R_AbsRing R_NormedModule R_NormedModule sqrt (@locally R_UniformSpace x) (fun y : NormedModule.sort R_AbsRing R_NormedModule => @scal R_Ring R_ModuleSpace y (Rinv (Rmult (IZR (Zpos (xO xH))) (sqrt x)))) *)
      apply is_derive_Reals.
      apply derivable_pt_lim_minus.
      apply derivable_pt_lim_id.
      apply derivable_pt_lim_ln.
      eapply Rlt_trans, Hz.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
      apply Rmin_case => //.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
      by apply Rlt_0_1.
      rewrite /l ; field.
      apply Rgt_not_eq ; eapply Rlt_trans, Hz.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
      apply Rmin_case => //.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
      by apply Rlt_0_1.
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
    move => y Hy.
    apply continuity_pt_minus.
    apply continuity_pt_id.
    apply derivable_continuous_pt ;
    eexists ; apply derivable_pt_lim_ln.
    eapply Rlt_le_trans, Hy.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
      apply Rmin_case => //.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
      by apply Rlt_0_1.
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
    move => c [Hc H0].
    replace 1 with (1 - ln 1) by (rewrite ln_1 Rminus_0_r //).
    apply Rminus_le_0.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    rewrite H0.
    move: Hc ; rewrite /Rmin /Rmax ; case: Rle_dec => H1 Hc.
(* Goal: Rle (IZR Z0) (Rmult (Rinv (INR (fact (S n)))) (pow x (S n))) *)
    apply Rmult_le_pos.
    apply Rdiv_le_0_compat.
    apply -> Rminus_le_0 ; apply Hc.
    apply Rlt_le_trans with (1 := Rlt_0_1).
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    by apply Hc.
    apply -> Rminus_le_0 ; apply H1.
    apply Rnot_le_lt in H1.
    replace ((c - 1) / c * (x - 1)) with ((1-c) * (1-x) / c).
    apply Rdiv_le_0_compat.
(* Goal: Rle (IZR Z0) (Rmult (Rinv (INR (fact (S n)))) (pow x (S n))) *)
    apply Rmult_le_pos.
    apply -> Rminus_le_0 ; apply Hc.
    apply -> Rminus_le_0 ; apply Rlt_le, H1.
    apply Rlt_le_trans with (1 := Hx).
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    by apply Hc.
    field.
    apply Rgt_not_eq.
    apply Rlt_le_trans with (1 := Hx).
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    by apply Hc.
  apply (is_lim_le_le_loc (fun _ => 0) (fun y => 2/sqrt y)).
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists 1 => x Hx.
(* Goal: and (Rle (IZR Z0) (Rsqr (Rmax (IZR Z0) M))) (Rlt (Rsqr (Rmax (IZR Z0) M)) x) *)
(* Goal: Rle (IZR Z0) (Rmax (IZR Z0) M) *)
  split.
  apply Rdiv_le_0_compat.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -ln_1.
  apply ln_le.
  apply Rlt_0_1.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rlt_le.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rlt_trans with (1 := Rlt_0_1).
  replace (ln _) with (2 * ln (sqrt x)).
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /Rdiv Rmult_assoc.
  apply Rmult_le_compat_l.
  apply Rlt_le, Rlt_0_2.
  apply Rle_div_l.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rlt_trans with (1 := Rlt_0_1).
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -{3}(sqrt_sqrt x).
  field_simplify ; rewrite ?Rdiv_1.
  apply Rlt_le, H.
  apply sqrt_lt_R0.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rlt_trans with (1 := Rlt_0_1).
  apply Rgt_not_eq.
  apply sqrt_lt_R0.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rlt_trans with (1 := Rlt_0_1).
  apply Rlt_le.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rlt_trans with (1 := Rlt_0_1).
  change 2 with (INR 2).
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -ln_pow.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /= Rmult_1_r.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite sqrt_sqrt.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by [].
  apply Rlt_le.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rlt_trans with (1 := Rlt_0_1).
  apply sqrt_lt_R0.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rlt_trans with (1 := Rlt_0_1).
  apply is_lim_const.
  evar_last.
  apply is_lim_div.
  apply is_lim_const.
  apply filterlim_sqrt_p.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by [].
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by [].
  simpl ; by rewrite Rmult_0_r.
Qed.

Lemma is_lim_div_ln1p_0 : is_lim (fun y => ln (1+y) / y) 0 1.
Proof.
(* Goal: is_lim (fun x : R => Rdiv (sin x) x) (Finite (IZR Z0)) (Finite (IZR (Zpos xH))) *)
  apply is_lim_spec.
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
  move => eps.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: (derivable_pt_lim_ln 1 (Rlt_0_1) eps (cond_pos eps)) => delta H.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists delta => y Hy Hy0.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /= in Hy.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /= -/(Rminus _ _) Rminus_0_r in Hy.
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
  move: (H y Hy0 Hy).
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by rewrite ln_1 Rinv_1 Rminus_0_r.
Qed.

(** * Unnormalized sinc *)

Lemma is_lim_sinc_0 : is_lim (fun x => sin x / x) 0 1.
Proof.
(* Goal: is_lim (fun x : R => Rdiv (sin x) x) (Finite (IZR Z0)) (Finite (IZR (Zpos xH))) *)
  apply is_lim_spec.
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
  move => eps.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: (derivable_pt_lim_sin_0 eps (cond_pos eps)) => delta H.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  exists delta => y Hy Hy0.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /= in Hy.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /= -/(Rminus _ _) Rminus_0_r in Hy.
(* Goal: Rlt (Rabs (Rminus (Rdiv (sin y) y) (IZR (Zpos xH)))) (pos eps) *)
  move: (H y Hy0 Hy).
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by rewrite Rplus_0_l sin_0 Rminus_0_r.
Qed.

(** * ArcTan *)

Lemma CV_radius_atan : CV_radius (fun n => (-1)^n / (INR (S (n + n)))) = 1.
Proof.
  apply eq_trans with (2 := f_equal Finite Rinv_1).
  apply CV_radius_finite_DAlembert.
  intros n.
  apply Rmult_integral_contrapositive_currified.
  apply pow_nonzero.
  apply Rlt_not_eq, Rminus_lt_0 ; ring_simplify ; apply Rlt_0_1.
  rewrite S_INR ; by apply Rgt_not_eq, RinvN_pos.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rlt_0_1.
  apply is_lim_seq_ext with (fun n => 1 - 2 / (2 * INR n + 3)).
  intros n.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -plus_n_Sm plus_Sn_m !S_INR plus_INR.
  assert (0 < INR n + INR n + 1).
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    rewrite -plus_INR -S_INR.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    by apply (lt_INR O), lt_O_Sn.
  assert (0 < INR n + INR n + 1 + 1 + 1).
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    rewrite -plus_INR -!S_INR.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    by apply (lt_INR O), lt_O_Sn.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite !Rabs_div ; try by apply Rgt_not_eq.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -!RPow_abs Rabs_m1 !pow1 !Rabs_pos_eq ; try by left.
  field.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  split ; by apply Rgt_not_eq.
  apply Rmult_integral_contrapositive_currified.
  apply pow_nonzero.
  apply Rlt_not_eq, Rminus_lt_0 ; ring_simplify ; apply Rlt_0_1.
  rewrite -plus_INR ; by apply Rgt_not_eq, RinvN_pos.
  evar_last.
  apply is_lim_seq_minus'.
  apply filterlim_const.
  eapply is_lim_seq_div.
  apply is_lim_seq_const.
  eapply is_lim_seq_plus.
  eapply is_lim_seq_mult.
  apply is_lim_seq_const.
  apply is_lim_seq_INR.
  apply is_Rbar_mult_sym, is_Rbar_mult_p_infty_pos.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by apply Rlt_0_2.
  apply is_lim_seq_const.
  reflexivity ; simpl.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by [].
  reflexivity.
  simpl ; apply f_equal ; ring.
Qed.
Lemma atan_Reals (x : R) : Rabs x < 1
  -> atan x = x * PSeries (fun n => (-1)^n / (INR (S (n + n)))) (x ^ 2).
Proof.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  wlog: x / (0 <= x) => [Hw | Hx0] Hx.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    case: (Rle_lt_dec 0 x) => Hx0.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    by apply Hw.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    rewrite -{1}(Ropp_involutive x) atan_opp Hw.
(* Goal: @eq R (Ropp (Rmult (Ropp x) (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (Ropp x) (S (S O)))))) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: Rlt (Rabs (Ropp x)) (IZR (Zpos xH)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    replace ((- x) ^ 2) with (x^2) by ring.
(* Goal: @eq R (Ropp (Rmult (Ropp x) (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O)))))) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: Rlt (Rabs (Ropp x)) (IZR (Zpos xH)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    ring.
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: Rlt (Rabs (Ropp x)) (IZR (Zpos xH)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    apply Ropp_le_cancel ; rewrite Ropp_involutive Ropp_0 ; by left.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
    by rewrite Rabs_Ropp.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite Rabs_pos_eq // in Hx.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: Hx0 => Hx0.
(* Goal: and (Rle (IZR Z0) (Rsqr (Rmax (IZR Z0) M))) (Rlt (Rsqr (Rmax (IZR Z0) M)) x) *)
(* Goal: Rle (IZR Z0) (Rmax (IZR Z0) M) *)
  rewrite atan_eq_ps_atan ; try by split.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /ps_atan.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: Ratan.in_int => H.
(* Goal: @eq R (let (v, _) := ps_atan_exists_1 x H in v) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  case: ps_atan_exists_1 => ps Hps.
(* Goal: @eq R ps (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  apply sym_eq.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -Series.Series_scal_l.
(* Goal: @eq R (Series.Series (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n)))) ps *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  apply Series.is_series_unique.
(* Goal: @Series.is_series R_AbsRing R_NormedModule (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) ps *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  apply is_lim_seq_Reals in Hps.
(* Goal: @Series.is_series R_AbsRing R_NormedModule (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) ps *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  move: Hps ; apply is_lim_seq_ext => n.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -sum_n_Reals.
(* Goal: @eq R (@sum_n R_AbelianGroup (tg_alt (Ratan_seq x)) n) (@sum_n (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (fun n : nat => Rmult x (Rmult (Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow (pow x (S (S O))) n))) n) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  apply sum_n_ext => k.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite /tg_alt /Ratan_seq S_INR !plus_INR.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite pow_add -pow_mult.
  simpl ; field.
(* Goal: not (@eq R (Rplus (Rplus (INR k) (INR k)) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  rewrite -plus_INR -S_INR.
(* Goal: not (@eq R (INR (S (Init.Nat.add k k))) (IZR Z0)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  apply Rgt_not_eq, (lt_INR 0), lt_O_Sn.
(* Goal: and (Rle (IZR Z0) (Rsqr (Rmax (IZR Z0) M))) (Rlt (Rsqr (Rmax (IZR Z0) M)) x) *)
(* Goal: Rle (IZR Z0) (Rmax (IZR Z0) M) *)
  contradict H ; split.
(* Goal: Rle (IZR (Zneg xH)) x *)
(* Goal: Rle x (IZR (Zpos xH)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  apply Rle_trans with 0.
(* Goal: Rle (IZR (Zneg xH)) (IZR Z0) *)
(* Goal: Rle (IZR Z0) x *)
(* Goal: Rle x (IZR (Zpos xH)) *)
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  apply Rminus_le_0 ; ring_simplify ; by apply Rle_0_1.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by left.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by left.
(* Goal: @eq R (atan x) (Rmult x (PSeries (fun n : nat => Rdiv (pow (IZR (Zneg xH)) n) (INR (S (Init.Nat.add n n)))) (pow x (S (S O))))) *)
  by rewrite -Hx0 atan_0 Rmult_0_l.
Qed.
