Adds the proof of PI_ineq, plus some other smarter ways to approximate PI

and of course, the definition of atan (the inverse of tan, from R to
(-PI/2, PI/2)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15428 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 3121 insertions, 0 deletions

diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v
new file mode 100644
index 000000000..96f7cae8c
--- /dev/null
+++ b/theories/Reals/Machin.v
@@ -0,0 +1,168 @@
+Require Import Fourier.
+Require Import Rbase.
+Require Import Rtrigo.
+Require Import Ranalysis.
+Require Import Rfunctions.
+Require Import AltSeries.
+Require Import Rseries.
+Require Import SeqProp.
+Require Import PartSum.
+Require Import Ratan.
+
+Open Local Scope R_scope.
+
+(* Proving a few formulas in the style of John Machin to compute Pi *)
+
+Definition atan_sub u v := (u - v)/(1 + u * v).
+
+Lemma atan_sub_correct :
+ forall u v, 1 + u * v <> 0 -> -PI/2 < atan u - atan v < PI/2 ->
+   -PI/2 < atan (atan_sub u v) < PI/2 ->
+   atan u = atan v + atan (atan_sub u v).
+intros u v pn0 uvint aint.
+assert (cos (atan u) <> 0).
+ destruct (atan_bound u); apply Rgt_not_eq, cos_gt_0; auto.
+ rewrite <- Ropp_div; assumption.
+assert (cos (atan v) <> 0).
+ destruct (atan_bound v); apply Rgt_not_eq, cos_gt_0; auto.
+ rewrite <- Ropp_div; assumption.
+assert (t : forall a b c, a - b = c -> a = b + c) by (intros; subst; field).
+apply t, tan_is_inj; clear t; try assumption.
+rewrite tan_minus; auto.
+  rewrite !atan_right_inv; reflexivity.
+apply Rgt_not_eq, cos_gt_0; rewrite <- ?Ropp_div; tauto.
+rewrite !atan_right_inv; assumption.
+Qed.
+
+Lemma tech : forall x y , -1 <= x <= 1 -> -1 < y < 1 -> 
+  -PI/2 < atan x - atan y < PI/2.
+assert (ut := PI_RGT_0).
+intros x y [xm1 x1] [ym1 y1].
+assert (-(PI/4) <= atan x).
+ destruct xm1 as [xm1 | xm1].
+  rewrite <- atan_1, <- atan_opp; apply Rlt_le, atan_increasing.
+  assumption.
+ solve[rewrite <- xm1, atan_opp, atan_1; apply Rle_refl].
+assert (-(PI/4) < atan y).
+ rewrite <- atan_1, <- atan_opp; apply atan_increasing.
+ assumption.
+assert (atan x <= PI/4).
+ destruct x1 as [x1 | x1].
+  rewrite <- atan_1; apply Rlt_le, atan_increasing.
+  assumption.
+ solve[rewrite x1, atan_1; apply Rle_refl].
+assert (atan y < PI/4).
+  rewrite <- atan_1; apply atan_increasing.
+  assumption.
+rewrite Ropp_div; split; fourier.
+Qed.
+
+(* A simple formula, reasonably efficient. *)
+Lemma Machin_2_3 : PI/4 = atan(/2) + atan(/3).
+assert (utility : 0 < PI/2) by (apply PI2_RGT_0).
+rewrite <- atan_1.
+rewrite (atan_sub_correct 1 (/2)).
+   apply f_equal, f_equal; unfold atan_sub; field.
+  apply Rgt_not_eq; fourier.
+ apply tech; try split; try fourier.
+apply atan_bound.
+Qed.
+
+Lemma Machin_4_5_239 : PI/4 = 4 * atan (/5) - atan(/239).
+rewrite <- atan_1.
+rewrite (atan_sub_correct 1 (/5));
+ [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
+     apply atan_bound ].
+replace (4 * atan (/5) - atan (/239)) with
+  (atan (/5) + (atan (/5) + (atan (/5) + (atan (/5) + -
+     atan (/239))))) by ring.
+apply f_equal.
+replace (atan_sub 1 (/5)) with (2/3) by
+  (unfold atan_sub; field).
+rewrite (atan_sub_correct (2/3) (/5));
+ [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
+     apply atan_bound ].
+replace (atan_sub (2/3) (/5)) with (7/17)  by
+  (unfold atan_sub; field).
+rewrite (atan_sub_correct (7/17) (/5));
+ [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
+     apply atan_bound ].
+replace (atan_sub (7/17) (/5)) with (9/46) by
+  (unfold atan_sub; field).
+rewrite (atan_sub_correct (9/46) (/5));
+ [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
+     apply atan_bound ].
+rewrite <- atan_opp; apply f_equal.
+unfold atan_sub; field.
+Qed.
+
+Lemma Machin_2_3_7 : PI/4 = 2 * atan(/3) + (atan (/7)).
+rewrite <- atan_1.
+rewrite (atan_sub_correct 1 (/3));
+ [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
+     apply atan_bound ].
+replace (2 * atan (/3) + atan (/7)) with
+  (atan (/3) + (atan (/3) + atan (/7))) by ring.
+apply f_equal.
+replace (atan_sub 1 (/3)) with (/2) by
+  (unfold atan_sub; field).
+rewrite (atan_sub_correct (/2) (/3));
+ [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
+     apply atan_bound ].
+apply f_equal; unfold atan_sub; field.
+Qed.
+
+(* More efficient way to compute approximations of PI. *)
+
+Definition PI_2_3_7_tg n := 
+  2 * Ratan_seq (/3) n + Ratan_seq (/7) n.
+
+Lemma PI_2_3_7_ineq :
+  forall N : nat,
+    sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <= PI / 4 <=
+    sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N).
+Proof.
+assert (dec3 : 0 <= /3 <= 1) by (split; fourier).
+assert (dec7 : 0 <= /7 <= 1) by (split; fourier).
+assert (decr : Un_decreasing PI_2_3_7_tg).
+ apply Ratan_seq_decreasing in dec3.
+ apply Ratan_seq_decreasing in dec7.
+ intros n; apply Rplus_le_compat.
+  apply Rmult_le_compat_l; [ fourier | exact (dec3 n)].
+ exact (dec7 n).
+assert (cv : Un_cv PI_2_3_7_tg 0).
+ apply Ratan_seq_converging in dec3.
+ apply Ratan_seq_converging in dec7.
+ intros eps ep.
+ assert (ep' : 0 < eps /3) by fourier.
+ destruct (dec3 _ ep') as [N1 Pn1]; destruct (dec7 _ ep') as [N2 Pn2].
+ exists (N1 + N2)%nat; intros n Nn.
+ unfold PI_2_3_7_tg.
+ rewrite <- (Rplus_0_l 0).
+ apply Rle_lt_trans with
+    (1 := R_dist_plus (2 * Ratan_seq (/3) n) 0 (Ratan_seq (/7) n) 0).
+ replace eps with (2 * eps/3 + eps/3) by field.
+ apply Rplus_lt_compat.
+  unfold R_dist, Rminus, Rdiv.
+  rewrite <- (Rmult_0_r 2), <- Ropp_mult_distr_r_reverse.
+  rewrite <- Rmult_plus_distr_l, Rabs_mult, (Rabs_pos_eq 2);[|fourier].
+  rewrite Rmult_assoc; apply Rmult_lt_compat_l;[fourier | ].
+   apply (Pn1 n); omega.
+  apply (Pn2 n); omega.
+rewrite Machin_2_3_7.
+rewrite !atan_eq_ps_atan; try (split; fourier).
+unfold ps_atan; destruct (in_int (/3)); destruct (in_int (/7));
+  try match goal with id : ~ _ |- _ => case id; split; fourier end.
+destruct (ps_atan_exists_1 (/3)) as [v3 Pv3].
+destruct (ps_atan_exists_1 (/7)) as [v7 Pv7].
+assert (main : Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg)) (2 * v3 + v7)).
+ assert (main :Un_cv (fun n => 2 * sum_f_R0 (tg_alt (Ratan_seq (/3))) n +
+                        sum_f_R0 (tg_alt (Ratan_seq (/7))) n) (2 * v3 + v7)).
+  apply CV_plus;[ | assumption].
+  apply CV_mult;[ | assumption].
+  exists 0%nat; intros; rewrite R_dist_eq; assumption.
+ apply Un_cv_ext with (2 := main).
+ intros n; rewrite scal_sum, <- plus_sum; apply sum_eq; intros.
+ rewrite Rmult_comm; unfold PI_2_3_7_tg, tg_alt; field.
+intros N; apply (alternated_series_ineq _ _ _ decr cv main).
+Qed.
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
new file mode 100644
index 000000000..096559ac4
--- /dev/null
+++ b/theories/Reals/Ranalysis5.v
@@ -0,0 +1,1348 @@
+Require Import Rbase.
+Require Import Ranalysis.
+Require Import Rfunctions.
+Require Import Rseries.
+Require Import Fourier.
+Require Import RiemannInt.
+Require Import SeqProp.
+Require Import Max.
+Open Local Scope R_scope.
+
+(** * Preliminaries lemmas *)
+
+Lemma f_incr_implies_g_incr_interv : forall f g:R->R, forall lb ub,
+       lb < ub ->
+       (forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) ->
+       (forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x) ->
+       (forall x , f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
+       (forall x y, f lb <= x -> x < y -> y <= f ub -> g x < g y).
+Proof.
+intros f g lb ub lb_lt_ub f_incr f_eq_g g_ok x y lb_le_x x_lt_y y_le_ub.
+ assert (x_encad : f lb <= x <= f ub).
+  split ; [assumption | apply Rle_trans with (r2:=y) ; [apply Rlt_le|] ; assumption].
+ assert (y_encad : f lb <= y <= f ub).
+  split ; [apply Rle_trans with (r2:=x) ; [|apply Rlt_le] ; assumption | assumption].
+  assert (Temp1 : lb <= lb) by intuition ; assert (Temp2 : ub <= ub) by intuition.
+ assert (gx_encad := g_ok _ (proj1 x_encad) (proj2 x_encad)).
+ assert (gy_encad := g_ok _ (proj1 y_encad) (proj2 y_encad)).
+ clear Temp1 Temp2.
+ case (Rlt_dec (g x) (g y)).
+  intuition.
+  intros Hfalse.
+   assert (Temp := Rnot_lt_le _ _ Hfalse).
+   assert (Hcontradiction : y <= x).
+   replace y with (id y) by intuition ; replace x with (id x) by intuition ;
+   rewrite <- f_eq_g. rewrite <- f_eq_g.
+   assert (f_incr2 : forall x y, lb <= x -> x <= y -> y < ub -> f x <= f y).
+    intros m n lb_le_m m_le_n n_lt_ub.
+    case (m_le_n).
+     intros ; apply Rlt_le ; apply f_incr ; [| | apply Rlt_le] ; assumption.
+     intros Hyp ; rewrite Hyp ; apply Req_le ; reflexivity.
+   apply f_incr2.
+   intuition. intuition.
+   Focus 3. intuition.
+   Focus 2. intuition.
+   Focus 2. intuition. Focus 2. intuition.
+   assert (Temp2 : g x <> ub).
+   intro Hf.
+    assert (Htemp : (comp f g) x = f ub).
+     unfold comp ; rewrite Hf ; reflexivity.
+     rewrite f_eq_g in Htemp ; unfold id in Htemp.
+    assert (Htemp2 : x < f ub).
+     apply Rlt_le_trans with (r2:=y) ; intuition.
+    clear -Htemp Htemp2. fourier.
+    intuition. intuition.
+   clear -Temp2 gx_encad.
+   case (proj2 gx_encad).
+    intuition.
+    intro Hfalse ; apply False_ind ; apply Temp2 ; assumption.
+   apply False_ind. clear - Hcontradiction x_lt_y. fourier.
+Qed.
+
+Lemma derivable_pt_id_interv : forall (lb ub x:R),
+       lb <= x <= ub ->
+       derivable_pt id x.
+Proof.
+intros.
+ reg.
+Qed.
+
+Lemma pr_nu_var2_interv : forall (f g : R -> R) (lb ub x : R) (pr1 : derivable_pt f x)
+       (pr2 : derivable_pt g x),
+       lb < ub ->
+       lb < x < ub ->
+       (forall h : R, lb < h < ub -> f h = g h) -> derive_pt f x pr1 = derive_pt g x pr2.
+Proof.
+intros f g lb ub x Prf Prg lb_lt_ub x_encad local_eq.
+assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs g x l)).
+ intros a l a_encad.
+ unfold derivable_pt_abs, derivable_pt_lim.
+ split.
+ intros Hyp eps eps_pos.
+ elim (Hyp eps eps_pos) ; intros delta Hyp2.
+ assert (Pos_cond : Rmin delta (Rmin (ub - a) (a - lb)) > 0).
+  clear-a lb ub a_encad delta.
+  apply Rmin_pos ; [exact (delta.(cond_pos)) | apply Rmin_pos ] ; apply Rlt_Rminus ; intuition.
+ exists (mkposreal (Rmin delta (Rmin (ub - a) (a - lb))) Pos_cond).
+ intros h h_neq h_encad.
+ replace (g (a + h) - g a) with (f (a + h) - f a).
+ apply Hyp2 ; intuition.
+ apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))).
+ assumption. apply Rmin_l.
+ assert (local_eq2 : forall h : R, lb < h < ub -> - f h = - g h).
+  intros ; apply Ropp_eq_compat ; intuition.
+ rewrite local_eq ; unfold Rminus. rewrite local_eq2. reflexivity.
+ assumption.
+ assert (Sublemma2 : forall x y, Rabs x < Rabs y -> y > 0 -> x < y).
+  intros m n Hyp_abs y_pos. apply Rlt_le_trans with (r2:=Rabs n).
+   apply Rle_lt_trans with (r2:=Rabs m) ; [ | assumption] ; apply RRle_abs.
+   apply Req_le ; apply Rabs_right ; apply Rgt_ge ; assumption.
+ split.
+ assert (Sublemma : forall x y z, -z < y - x -> x < y + z).
+  intros ; fourier.
+ apply Sublemma.
+ apply Sublemma2. rewrite Rabs_Ropp.
+ apply Rlt_le_trans with (r2:=a-lb) ; [| apply RRle_abs] ;
+ apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ;
+ apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption.
+ apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ;
+ apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption.
+ assert (Sublemma : forall x y z, y < z - x -> x + y < z).
+  intros ; fourier.
+ apply Sublemma.
+ apply Sublemma2.
+ apply Rlt_le_trans with (r2:=ub-a) ; [| apply RRle_abs] ;
+ apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_l] ;
+ apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption.
+ apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_l] ;
+ apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption.
+ intros Hyp eps eps_pos.
+ elim (Hyp eps eps_pos) ; intros delta Hyp2.
+ assert (Pos_cond : Rmin delta (Rmin (ub - a) (a - lb)) > 0).
+  clear-a lb ub a_encad delta.
+  apply Rmin_pos ; [exact (delta.(cond_pos)) | apply Rmin_pos ] ; apply Rlt_Rminus ; intuition.
+ exists (mkposreal (Rmin delta (Rmin (ub - a) (a - lb))) Pos_cond).
+ intros h h_neq h_encad.
+ replace (f (a + h) - f a) with (g (a + h) - g a).
+ apply Hyp2 ; intuition.
+ apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))).
+ assumption. apply Rmin_l.
+ assert (local_eq2 : forall h : R, lb < h < ub -> - f h = - g h).
+  intros ; apply Ropp_eq_compat ; intuition.
+ rewrite local_eq ; unfold Rminus. rewrite local_eq2. reflexivity.
+ assumption.
+ assert (Sublemma2 : forall x y, Rabs x < Rabs y -> y > 0 -> x < y).
+  intros m n Hyp_abs y_pos. apply Rlt_le_trans with (r2:=Rabs n).
+   apply Rle_lt_trans with (r2:=Rabs m) ; [ | assumption] ; apply RRle_abs.
+   apply Req_le ; apply Rabs_right ; apply Rgt_ge ; assumption.
+ split.
+ assert (Sublemma : forall x y z, -z < y - x -> x < y + z).
+  intros ; fourier.
+ apply Sublemma.
+ apply Sublemma2. rewrite Rabs_Ropp.
+ apply Rlt_le_trans with (r2:=a-lb) ; [| apply RRle_abs] ;
+ apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ;
+ apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption.
+ apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ;
+ apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption.
+ assert (Sublemma : forall x y z, y < z - x -> x + y < z).
+  intros ; fourier.
+ apply Sublemma.
+ apply Sublemma2.
+ apply Rlt_le_trans with (r2:=ub-a) ; [| apply RRle_abs] ;
+ apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_l] ;
+ apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption.
+ apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_l] ;
+ apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption.
+ unfold derivable_pt in Prf.
+  unfold derivable_pt in Prg.
+  elim Prf; intros.
+  elim Prg; intros.
+  assert (Temp := p); rewrite H in Temp.
+  unfold derivable_pt_abs in p.
+  unfold derivable_pt_abs in p0.
+  simpl in |- *.
+  apply (uniqueness_limite g x x0 x1 Temp p0).
+  assumption.
+Qed.
+
+
+(* begin hide *)
+Lemma leftinv_is_rightinv : forall (f g:R->R),
+       (forall x y, x < y -> f x < f y) ->
+       (forall x, (comp f g) x = id x) ->
+       (forall x, (comp g f) x = id x).
+Proof.
+intros f g f_incr Hyp x.
+ assert (forall x, f (g (f x)) = f x).
+  intros ; apply Hyp.
+ assert(f_inj : forall x y, f x = f y -> x = y).
+  intros a b fa_eq_fb.
+  case(total_order_T a b).
+  intro s ; case s ; clear s.
+  intro Hf.
+  assert (Hfalse := f_incr a b Hf).
+  apply False_ind. apply (Rlt_not_eq (f a) (f b)) ; assumption.
+  intuition.
+  intro Hf. assert (Hfalse := f_incr b a Hf).
+  apply False_ind. apply (Rlt_not_eq (f b) (f a)) ; [|symmetry] ; assumption.
+ apply f_inj. unfold comp.
+ unfold comp in Hyp.
+ rewrite Hyp.
+ unfold id.
+ reflexivity.
+Qed.
+(* end hide *)
+
+Lemma leftinv_is_rightinv_interv : forall (f g:R->R) (lb ub:R),
+       (forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) ->
+       (forall y, f lb <= y -> y <= f ub -> (comp f g) y = id y) ->
+       (forall x, f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
+       forall x,
+       lb <= x <= ub ->
+       (comp g f) x = id x.
+Proof.
+intros f g lb ub f_incr_interv Hyp g_wf x x_encad.
+ assert(f_inj : forall x y, lb <= x <= ub -> lb <= y <= ub -> f x = f y -> x = y).
+  intros a b a_encad b_encad fa_eq_fb.
+  case(total_order_T a b).
+  intro s ; case s ; clear s.
+  intro Hf.
+  assert (Hfalse := f_incr_interv a b (proj1 a_encad) Hf (proj2 b_encad)).
+  apply False_ind. apply (Rlt_not_eq (f a) (f b)) ; assumption.
+  intuition.
+  intro Hf. assert (Hfalse := f_incr_interv b a (proj1 b_encad) Hf (proj2 a_encad)).
+  apply False_ind. apply (Rlt_not_eq (f b) (f a)) ; [|symmetry] ; assumption.
+ assert (f_incr_interv2 : forall x y, lb <= x -> x <= y -> y <= ub -> f x <= f y).
+  intros m n cond1 cond2 cond3.
+   case cond2.
+   intro cond. apply Rlt_le ; apply f_incr_interv ; assumption.
+   intro cond ; right ; rewrite cond ; reflexivity.
+ assert (Hyp2:forall x, lb <= x <= ub -> f (g (f x)) = f x).
+  intros ; apply Hyp.  apply f_incr_interv2 ; intuition. 
+ apply f_incr_interv2 ; intuition.
+ unfold comp ; unfold comp in Hyp.
+ apply f_inj.
+ apply g_wf ; apply f_incr_interv2 ; intuition.
+ unfold id ; assumption.
+ apply Hyp2 ; unfold id ; assumption.
+Qed.
+
+
+(** Intermediate Value Theorem on an Interval (Proof mainly taken from Reals.Rsqrt_def) and its corollary *)
+
+Lemma IVT_interv_prelim0 : forall (x y:R) (P:R->bool) (N:nat),
+       x < y ->
+       x <= Dichotomy_ub x y P N <= y /\ x <= Dichotomy_lb x y P N <= y.
+Proof.
+assert (Sublemma : forall x y lb ub, lb <= x <= ub /\ lb <= y <= ub -> lb <= (x+y) / 2 <= ub).
+ intros x y lb ub Hyp.
+  split.
+  replace lb with ((lb + lb) * /2) by field.
+  unfold Rdiv ; apply Rmult_le_compat_r ; intuition.
+  replace ub with ((ub + ub) * /2) by field.
+  unfold Rdiv ; apply Rmult_le_compat_r ; intuition.
+intros x y P N x_lt_y.
+induction N.
+ simpl ; intuition.
+ simpl.
+ case (P ((Dichotomy_lb x y P N + Dichotomy_ub x y P N) / 2)).
+ split. apply Sublemma ; intuition.
+ intuition.
+ split. intuition.
+ apply Sublemma ; intuition.
+Qed.
+
+Lemma IVT_interv_prelim1 : forall (x y x0:R) (D : R -> bool),
+       x < y ->
+       Un_cv (dicho_up x y D) x0 ->
+       x <= x0 <= y.
+Proof.
+intros x y x0 D x_lt_y bnd.
+ assert (Main : forall n, x <= dicho_up x y D n <= y).
+  intro n. unfold dicho_up.
+  apply (proj1 (IVT_interv_prelim0 x y D n x_lt_y)).
+ split.
+  apply Rle_cv_lim with (Vn:=dicho_up x y D) (Un:=fun n => x).
+  intro n ; exact (proj1 (Main n)).
+  unfold Un_cv ; intros ; exists 0%nat ; intros ; unfold R_dist ; replace (x -x) with 0 by field ; rewrite Rabs_R0 ; assumption.
+  assumption.
+  apply Rle_cv_lim with (Un:=dicho_up x y D) (Vn:=fun n => y).
+  intro n ; exact (proj2 (Main n)).
+  assumption.
+  unfold Un_cv ; intros ; exists 0%nat ; intros ; unfold R_dist ; replace (y -y) with 0 by field ; rewrite Rabs_R0 ; assumption.
+Qed.
+
+Lemma IVT_interv : forall (f : R -> R) (x y : R),
+       (forall a, x <= a <= y -> continuity_pt f a) ->
+       x < y ->
+       f x < 0 ->
+       0 < f y ->
+       {z : R | x <= z <= y /\ f z = 0}.
+Proof.
+intros. (* f x y f_cont_interv x_lt_y fx_neg fy_pos.*)
+  cut (x <= y).
+  intro.
+  generalize (dicho_lb_cv x y (fun z:R => cond_positivity (f z)) H3). 
+  generalize (dicho_up_cv x y (fun z:R => cond_positivity (f z)) H3). 
+  intros X X0.
+  elim X; intros.
+  elim X0; intros.
+  assert (H4 := cv_dicho _ _ _ _ _ H3 p0 p).
+  rewrite H4 in p0.
+  exists x0.
+  split.
+  split.
+  apply Rle_trans with (dicho_lb x y (fun z:R => cond_positivity (f z)) 0).
+  simpl in |- *.
+  right; reflexivity.
+  apply growing_ineq.
+  apply dicho_lb_growing; assumption.
+  assumption.
+  apply Rle_trans with (dicho_up x y (fun z:R => cond_positivity (f z)) 0).
+  apply decreasing_ineq.
+  apply dicho_up_decreasing; assumption.
+  assumption.
+  right; reflexivity.
+  2: left; assumption.
+  set (Vn := fun n:nat => dicho_lb x y (fun z:R => cond_positivity (f z)) n).
+  set (Wn := fun n:nat => dicho_up x y (fun z:R => cond_positivity (f z)) n).
+  cut ((forall n:nat, f (Vn n) <= 0) -> f x0 <= 0).
+  cut ((forall n:nat, 0 <= f (Wn n)) -> 0 <= f x0).
+  intros.
+  cut (forall n:nat, f (Vn n) <= 0).
+  cut (forall n:nat, 0 <= f (Wn n)).
+  intros.
+  assert (H9 := H6 H8).
+  assert (H10 := H5 H7).
+  apply Rle_antisym; assumption.
+  intro.
+  unfold Wn in |- *.
+  cut (forall z:R, cond_positivity z = true <-> 0 <= z).
+  intro.
+  assert (H8 := dicho_up_car x y (fun z:R => cond_positivity (f z)) n).
+  elim (H7 (f (dicho_up x y (fun z:R => cond_positivity (f z)) n))); intros.
+  apply H9.
+  apply H8.
+  elim (H7 (f y)); intros.
+  apply H12.
+  left; assumption.
+  intro.
+  unfold cond_positivity in |- *.
+  case (Rle_dec 0 z); intro.
+  split.
+  intro; assumption.
+  intro; reflexivity.
+  split.
+  intro feqt;discriminate feqt.
+  intro.
+  elim n0; assumption.
+  unfold Vn in |- *.
+  cut (forall z:R, cond_positivity z = false <-> z < 0).
+  intros.
+  assert (H8 := dicho_lb_car x y (fun z:R => cond_positivity (f z)) n).
+  left.
+  elim (H7 (f (dicho_lb x y (fun z:R => cond_positivity (f z)) n))); intros.
+  apply H9.
+  apply H8.
+  elim (H7 (f x)); intros.
+  apply H12.
+  assumption.
+  intro.
+  unfold cond_positivity in |- *.
+  case (Rle_dec 0 z); intro.
+  split.
+  intro feqt; discriminate feqt.
+  intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H7)).
+  split.
+  intro; auto with real.
+  intro; reflexivity.
+  cut (Un_cv Wn x0).
+  intros.
+  assert (Temp : x <= x0 <= y).
+   apply IVT_interv_prelim1 with (D:=(fun z : R => cond_positivity (f z))) ; assumption.
+  assert (H7 := continuity_seq f Wn x0 (H x0 Temp) H5).
+  case (total_order_T 0 (f x0)); intro.
+  elim s; intro.
+  left; assumption.
+  rewrite <- b; right; reflexivity.
+  unfold Un_cv in H7; unfold R_dist in H7.
+  cut (0 < - f x0).
+  intro.
+  elim (H7 (- f x0) H8); intros.
+  cut (x2 >= x2)%nat; [ intro | unfold ge in |- *; apply le_n ].
+  assert (H11 := H9 x2 H10).
+  rewrite Rabs_right in H11.
+  pattern (- f x0) at 1 in H11; rewrite <- Rplus_0_r in H11.
+  unfold Rminus in H11; rewrite (Rplus_comm (f (Wn x2))) in H11.
+  assert (H12 := Rplus_lt_reg_r _ _ _ H11).
+  assert (H13 := H6 x2).
+  elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H13 H12)).
+  apply Rle_ge; left; unfold Rminus in |- *; apply Rplus_le_lt_0_compat.
+  apply H6.
+  exact H8.
+  apply Ropp_0_gt_lt_contravar; assumption.
+  unfold Wn in |- *; assumption.
+  cut (Un_cv Vn x0).
+  intros.
+  assert (Temp : x <= x0 <= y).
+   apply IVT_interv_prelim1 with (D:=(fun z : R => cond_positivity (f z))) ; assumption.
+  assert (H7 := continuity_seq f Vn x0 (H x0 Temp) H5).
+  case (total_order_T 0 (f x0)); intro.
+  elim s; intro.
+  unfold Un_cv in H7; unfold R_dist in H7.
+  elim (H7 (f x0) a); intros.
+  cut (x2 >= x2)%nat; [ intro | unfold ge in |- *; apply le_n ].
+  assert (H10 := H8 x2 H9).
+  rewrite Rabs_left in H10.
+  pattern (f x0) at 2 in H10; rewrite <- Rplus_0_r in H10.
+  rewrite Ropp_minus_distr' in H10.
+  unfold Rminus in H10.
+  assert (H11 := Rplus_lt_reg_r _ _ _ H10).
+  assert (H12 := H6 x2).
+  cut (0 < f (Vn x2)).
+  intro.
+  elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H13 H12)).
+  rewrite <- (Ropp_involutive (f (Vn x2))).
+  apply Ropp_0_gt_lt_contravar; assumption.
+  apply Rplus_lt_reg_r with (f x0 - f (Vn x2)).
+  rewrite Rplus_0_r; replace (f x0 - f (Vn x2) + (f (Vn x2) - f x0)) with 0;
+    [ unfold Rminus in |- *; apply Rplus_lt_le_0_compat | ring ].
+  assumption.
+  apply Ropp_0_ge_le_contravar; apply Rle_ge; apply H6.
+  right; rewrite <- b; reflexivity.
+  left; assumption.
+  unfold Vn in |- *; assumption.
+Qed.
+
+(* begin hide *)
+Ltac case_le H :=
+   let t := type of H in 
+   let h' := fresh in 
+      match t with ?x <= ?y => case (total_order_T x y);
+         [intros h'; case h'; clear h' | 
+          intros h'; clear -H h'; elimtype False; fourier ] end.
+(* end hide *)
+
+
+Lemma f_interv_is_interv : forall (f:R->R) (lb ub y:R),
+       lb < ub ->
+       f lb <= y <= f ub ->
+       (forall x, lb <=  x <= ub -> continuity_pt f x) ->
+       {x | lb <= x <= ub /\ f x = y}.
+Proof.
+intros f lb ub y lb_lt_ub y_encad f_cont_interv.
+ case y_encad ; intro y_encad1.
+   case_le y_encad1 ; intros y_encad2 y_encad3 ; case_le y_encad3.
+    intro y_encad4.
+     clear y_encad y_encad1 y_encad3.
+     assert (Cont : forall a : R, lb <= a <= ub -> continuity_pt (fun x => f x - y) a).
+      intros a a_encad. unfold continuity_pt, continue_in, limit1_in, limit_in ; simpl ; unfold R_dist.
+      intros eps eps_pos. elim (f_cont_interv a a_encad eps eps_pos).
+      intros alpha alpha_pos. destruct alpha_pos as (alpha_pos,Temp).
+      exists alpha. split.
+      assumption. intros x  x_cond.
+      replace (f x - y - (f a - y)) with (f x - f a) by field.
+      exact (Temp x x_cond).
+     assert (H1 : (fun x : R => f x - y) lb < 0).
+       apply Rlt_minus. assumption.
+      assert (H2 : 0 < (fun x : R => f x - y) ub).
+       apply Rgt_minus ; assumption.
+     destruct (IVT_interv (fun x => f x - y) lb ub Cont lb_lt_ub H1 H2) as (x,Hx).
+     exists x.
+     destruct Hx as (Hyp,Result).
+     intuition.
+     intro H ; exists ub ; intuition.
+     intro H ; exists lb ; intuition.
+     intro H ; exists ub ; intuition.
+Qed.
+
+(** ** The derivative of a reciprocal function       *)
+
+
+(** * Continuity of the reciprocal function *)
+
+Lemma continuity_pt_recip_prelim : forall (f g:R->R) (lb ub : R) (Pr1:lb < ub),
+       (forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) ->
+       (forall x, lb <= x <= ub -> (comp g f) x = id x) ->
+       (forall a, lb <= a <= ub -> continuity_pt f a) ->
+       forall b,
+       f lb < b < f ub ->
+       continuity_pt g b.
+Proof.
+assert (Sublemma : forall x y z, Rmax x y < z <-> x < z /\ y < z).
+ intros x y z. split.
+  unfold Rmax. case (Rle_dec x y) ; intros Hyp Hyp2.
+  split. apply Rle_lt_trans with (r2:=y) ; assumption. assumption.
+  split. assumption. apply Rlt_trans with (r2:=x).
+  assert (Temp : forall x y, ~ x <= y -> x > y).
+   intros m n Hypmn. intuition.
+  apply Temp ; clear Temp ; assumption.
+  assumption.
+  intros Hyp.
+  unfold Rmax. case (Rle_dec x y).
+  intro ; exact (proj2 Hyp).
+  intro ; exact (proj1 Hyp).
+assert (Sublemma2 : forall x y z, Rmin x y > z <-> x > z /\ y > z).
+ intros x y z. split.
+  unfold Rmin. case (Rle_dec x y) ; intros Hyp Hyp2.
+  split. assumption.
+  apply Rlt_le_trans with (r2:=x) ; intuition.
+  split.
+  apply Rlt_trans with (r2:=y). intuition.
+  assert (Temp : forall x y, ~ x <= y -> x > y).
+   intros m n Hypmn. intuition.
+  apply Temp ; clear Temp ; assumption.
+  assumption.
+  intros Hyp.
+  unfold Rmin. case (Rle_dec x y).
+  intro ; exact (proj1 Hyp).
+  intro ; exact (proj2 Hyp).
+assert (Sublemma3 : forall x y, x <= y /\ x <> y -> x < y).
+ intros m n Hyp. unfold Rle in Hyp.
+  destruct Hyp as (Hyp1,Hyp2).
+  case Hyp1.
+  intuition.
+  intro Hfalse ; apply False_ind ; apply Hyp2 ; exact Hfalse.
+intros f g lb ub lb_lt_ub f_incr_interv f_eq_g f_cont_interv b b_encad.
+ assert (f_incr_interv2 : forall x y, lb <= x -> x <= y -> y <= ub -> f x <= f y).
+  intros m n cond1 cond2 cond3.
+   case cond2.
+   intro cond. apply Rlt_le ; apply f_incr_interv ; assumption.
+   intro cond ; right ; rewrite cond ; reflexivity.
+ unfold continuity_pt, continue_in, limit1_in, limit_in ; intros eps eps_pos.
+ unfold dist ; simpl ; unfold R_dist.
+ assert (b_encad_e : f lb <= b <= f ub) by intuition.
+ elim (f_interv_is_interv f lb ub b lb_lt_ub b_encad_e f_cont_interv) ; intros x Temp.
+ destruct Temp as (x_encad,f_x_b).
+ assert (lb_lt_x : lb < x).
+ assert (Temp : x <> lb).
+  intro Hfalse.
+  assert (Temp' : b = f lb).
+   rewrite <- f_x_b ; rewrite Hfalse ; reflexivity.
+  assert (Temp'' : b <> f lb).
+   apply Rgt_not_eq ; exact (proj1 b_encad).
+  apply Temp'' ; exact Temp'.
+ apply Sublemma3.
+ split. exact (proj1 x_encad).
+ assert (Temp2 : forall x y:R, x <> y <-> y <> x).
+  intros m n. split ; intuition.
+ rewrite Temp2 ; assumption.
+ assert (x_lt_ub : x < ub).
+ assert (Temp : x <> ub).
+  intro Hfalse.
+  assert (Temp' : b = f ub).
+   rewrite <- f_x_b ; rewrite Hfalse ; reflexivity.
+  assert (Temp'' : b <> f ub).
+   apply Rlt_not_eq ; exact (proj2 b_encad).
+  apply Temp'' ; exact Temp'.
+ apply Sublemma3.
+ split ; [exact (proj2 x_encad) | assumption].
+ pose (x1 := Rmax (x - eps) lb).
+ pose (x2 := Rmin (x + eps) ub).
+ assert (Hx1 : x1 = Rmax (x - eps) lb) by intuition.
+ assert (Hx2 : x2 = Rmin (x + eps) ub) by intuition.
+ assert (x1_encad : lb <= x1 <= ub).
+  split. apply RmaxLess2.
+  apply Rlt_le. rewrite Hx1. rewrite Sublemma.
+  split. apply Rlt_trans with (r2:=x) ; fourier.
+  assumption.
+ assert (x2_encad : lb <= x2 <= ub).
+  split. apply Rlt_le ; rewrite Hx2 ; apply Rgt_lt ; rewrite Sublemma2.
+  split. apply Rgt_trans with (r2:=x) ; fourier.
+  assumption.
+  apply Rmin_r.
+ assert (x_lt_x2 : x < x2).
+  rewrite Hx2.
+  apply Rgt_lt. rewrite Sublemma2.
+  split ; fourier.
+ assert (x1_lt_x : x1 < x).
+  rewrite Hx1.
+  rewrite Sublemma.
+  split ; fourier.
+ exists (Rmin (f x - f x1) (f x2 - f x)).
+ split. apply Rmin_pos ; apply Rgt_minus. apply f_incr_interv ; [apply RmaxLess2 | | ] ; fourier.
+ apply f_incr_interv ; intuition.
+ intros y Temp.
+ destruct Temp as (_,y_cond).
+  rewrite <- f_x_b in y_cond.
+  assert (Temp : forall x y d1 d2, d1 > 0 -> d2 > 0 -> Rabs (y - x) < Rmin d1 d2 -> x - d1 <= y <= x + d2).
+   intros.
+    split. assert (H10 : forall x y z, x - y <= z -> x - z <= y). intuition. fourier.
+    apply H10. apply Rle_trans with (r2:=Rabs (y0 - x0)).
+    replace (Rabs (y0 - x0)) with (Rabs (x0 - y0)). apply RRle_abs.
+    rewrite <- Rabs_Ropp. unfold Rminus ; rewrite Ropp_plus_distr. rewrite Ropp_involutive.
+    intuition.
+    apply Rle_trans with (r2:= Rmin d1 d2). apply Rlt_le ; assumption.
+    apply Rmin_l.
+    assert (H10 : forall x y z, x - y <= z -> x <= y + z). intuition. fourier.
+    apply H10. apply Rle_trans with (r2:=Rabs (y0 - x0)). apply RRle_abs.
+    apply Rle_trans with (r2:= Rmin d1 d2). apply Rlt_le ; assumption.
+    apply Rmin_r.
+  assert (Temp' := Temp (f x) y (f x - f x1) (f x2 - f x)).
+  replace (f x - (f x - f x1)) with (f x1) in Temp' by field.
+  replace (f x + (f x2 - f x)) with (f x2) in Temp' by field.
+  assert (T : f x - f x1 > 0).
+   apply Rgt_minus. apply f_incr_interv ; intuition.
+  assert (T' : f x2 - f x > 0).
+   apply Rgt_minus. apply f_incr_interv ; intuition.
+  assert (Main := Temp' T T' y_cond).
+  clear Temp Temp' T T'.
+  assert (x1_lt_x2 : x1 < x2).
+   apply Rlt_trans with (r2:=x) ; assumption.
+   assert (f_cont_myinterv : forall a : R, x1 <= a <= x2 -> continuity_pt f a).
+    intros ; apply f_cont_interv ; split. 
+    apply Rle_trans with (r2 := x1) ; intuition.
+    apply Rle_trans with (r2 := x2) ; intuition.
+   elim (f_interv_is_interv f x1 x2 y x1_lt_x2 Main f_cont_myinterv) ; intros x' Temp.
+   destruct Temp as (x'_encad,f_x'_y).
+   rewrite <- f_x_b ; rewrite <- f_x'_y.
+   unfold comp in f_eq_g. rewrite f_eq_g. rewrite f_eq_g.
+   unfold id.
+   assert (x'_encad2 : x - eps <= x' <= x + eps).
+    split.
+    apply Rle_trans with (r2:=x1) ; [ apply RmaxLess1|] ; intuition.
+    apply Rle_trans with (r2:=x2) ; [ | apply Rmin_l] ; intuition.
+    assert (x1_lt_x' : x1 < x').
+     apply Sublemma3.
+     assert (x1_neq_x' : x1 <> x').
+      intro Hfalse. rewrite Hfalse, f_x'_y in y_cond.
+      assert (Hf : Rabs (y - f x) < f x - y).
+       apply Rlt_le_trans with (r2:=Rmin (f x - y) (f x2 - f x)). fourier.
+       apply Rmin_l.
+      assert(Hfin : f x - y < f x - y).
+       apply Rle_lt_trans with (r2:=Rabs (y - f x)).
+       replace (Rabs (y - f x)) with (Rabs (f x - y)). apply RRle_abs.
+       rewrite <- Rabs_Ropp. replace (- (f x - y)) with (y - f x) by field ; reflexivity. fourier.
+      apply (Rlt_irrefl (f x - y)) ; assumption.
+      split ; intuition.
+     assert (x'_lb : x - eps < x').
+      apply Sublemma3.
+      split. intuition. apply Rlt_not_eq.
+      apply Rle_lt_trans with (r2:=x1) ; [ apply RmaxLess1|] ; intuition.
+     assert (x'_lt_x2 : x' < x2).
+     apply Sublemma3.
+     assert (x1_neq_x' : x' <> x2).
+      intro Hfalse. rewrite <- Hfalse, f_x'_y in y_cond.
+      assert (Hf : Rabs (y - f x) < y - f x).
+       apply Rlt_le_trans with (r2:=Rmin (f x - f x1) (y - f x)). fourier.
+       apply Rmin_r.
+      assert(Hfin : y - f x < y - f x).
+       apply Rle_lt_trans with (r2:=Rabs (y - f x)). apply RRle_abs. fourier.
+      apply (Rlt_irrefl (y - f x)) ; assumption.
+      split ; intuition.
+     assert (x'_ub : x' < x + eps).
+      apply Sublemma3.
+      split. intuition. apply Rlt_not_eq.
+      apply Rlt_le_trans with (r2:=x2) ; [ |rewrite Hx2 ; apply Rmin_l] ; intuition.
+    apply Rabs_def1 ; fourier.
+    assumption.
+    split. apply Rle_trans with (r2:=x1) ; intuition.
+    apply Rle_trans with (r2:=x2) ; intuition.
+Qed.
+
+Lemma continuity_pt_recip_interv : forall (f g:R->R) (lb ub : R) (Pr1:lb < ub),
+       (forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) ->
+       (forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x) ->
+       (forall x, f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
+       (forall a, lb <= a <= ub -> continuity_pt f a) ->
+       forall b,
+       f lb < b < f ub ->
+       continuity_pt g b.
+Proof.
+intros f g lb ub lb_lt_ub f_incr_interv f_eq_g g_wf.
+assert (g_eq_f_prelim := leftinv_is_rightinv_interv f g lb ub f_incr_interv f_eq_g).
+assert (g_eq_f : forall x, lb <= x <= ub -> (comp g f) x = id x).
+intro x ; apply g_eq_f_prelim ; assumption.
+apply (continuity_pt_recip_prelim f g lb ub lb_lt_ub f_incr_interv g_eq_f).
+Qed.
+
+(** *   Derivability of the reciprocal function        *)
+
+Lemma derivable_pt_lim_recip_interv : forall (f g:R->R) (lb ub x:R)
+       (Prf:forall a : R, g lb <= a <= g ub -> derivable_pt f a) (Prg : continuity_pt g x),
+       lb < ub ->
+       lb < x < ub ->
+       forall (Prg_incr:g lb <= g x <= g ub),
+       (forall x, lb <= x <= ub -> (comp f g) x = id x) ->
+       derive_pt f (g x) (Prf (g x) Prg_incr) <> 0 ->
+       derivable_pt_lim g x (1 / derive_pt f (g x) (Prf (g x) Prg_incr)).
+Proof.
+intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq.
+ assert (x_encad2 : lb <= x <= ub).
+  split ; apply Rlt_le ; intuition.
+ elim (Prf (g x)); simpl; intros l Hl.
+ unfold derivable_pt_lim.
+ intros eps eps_pos.
+  pose (y := g x).
+   assert (Hlinv := limit_inv).
+    assert (Hf_deriv : forall eps:R,
+    0 < eps ->
+    exists delta : posreal,
+    (forall h:R,
+    h <> 0 -> Rabs h < delta -> Rabs ((f (g x + h) - f (g x)) / h - l) < eps)).
+     intros eps0 eps0_pos.
+      red in Hl ; red in Hl. elim (Hl eps0 eps0_pos).
+      intros deltatemp Htemp.
+       exists deltatemp ; exact Htemp.
+    elim (Hf_deriv eps eps_pos).
+    intros deltatemp Htemp.
+     red in Hlinv ; red in Hlinv ; simpl dist in Hlinv ; unfold R_dist in Hlinv.
+     assert (Hlinv' := Hlinv (fun h => (f (y+h) - f y)/h) (fun h => h <>0) l 0).
+     unfold limit1_in, limit_in, dist in Hlinv' ; simpl in Hlinv'. unfold R_dist in Hlinv'.
+     assert (Premisse : (forall eps : R,
+     eps > 0 ->
+     exists alp : R,
+     alp > 0 /\
+     (forall x : R,
+     (fun h => h <>0) x /\ Rabs (x - 0) < alp ->
+     Rabs ((f (y + x) - f y) / x - l) < eps))).
+      intros eps0 eps0_pos.
+       elim (Hf_deriv eps0 eps0_pos).
+       intros deltatemp' Htemp'.
+        exists deltatemp'.
+        split.
+         exact deltatemp'.(cond_pos).
+         intros htemp cond.
+          apply (Htemp' htemp).
+          exact (proj1 cond).
+         replace (htemp) with (htemp - 0).
+         exact (proj2 cond).
+         intuition.
+     assert (Premisse2 : l <> 0).
+      intro l_null.
+       rewrite l_null in Hl.
+       apply df_neq.
+       rewrite derive_pt_eq.
+       exact Hl.                
+     elim (Hlinv' Premisse Premisse2 eps eps_pos).
+     intros alpha cond.
+      assert (alpha_pos := proj1 cond) ; assert (inv_cont := proj2 cond) ; clear cond.
+      unfold derivable, derivable_pt, derivable_pt_abs, derivable_pt_lim in Prf.
+      elim (Hl eps eps_pos).
+      intros delta f_deriv.
+       assert (g_cont := g_cont_pur).
+       unfold continuity_pt, continue_in, limit1_in, limit_in in g_cont.
+       pose (mydelta := Rmin delta alpha).
+       assert (mydelta_pos : mydelta > 0).
+        unfold mydelta, Rmin.
+        case (Rle_dec delta alpha).
+        intro ; exact (delta.(cond_pos)).
+        intro ; exact alpha_pos.
+       elim (g_cont mydelta mydelta_pos).
+       intros delta' new_g_cont.
+        assert(delta'_pos := proj1 (new_g_cont)).
+        clear g_cont ; assert (g_cont := proj2 (new_g_cont)) ; clear new_g_cont.
+        pose (mydelta'' := Rmin delta' (Rmin (x - lb) (ub - x))).
+        assert(mydelta''_pos : mydelta'' > 0).
+         unfold mydelta''.
+         apply Rmin_pos ; [intuition | apply Rmin_pos] ; apply Rgt_minus ; intuition.
+        pose (delta'' := mkposreal mydelta'' mydelta''_pos: posreal).
+        exists delta''.
+        intros h h_neq h_le_delta'.
+  assert (lb <= x +h <= ub).
+ assert (Sublemma2 : forall x y, Rabs x < Rabs y -> y > 0 -> x < y).
+  intros m n Hyp_abs y_pos. apply Rlt_le_trans with (r2:=Rabs n).
+   apply Rle_lt_trans with (r2:=Rabs m) ; [ | assumption] ; apply RRle_abs.
+   apply Req_le ; apply Rabs_right ; apply Rgt_ge ; assumption.
+ assert (lb <= x + h <= ub).
+ split.
+ assert (Sublemma : forall x y z, -z <= y - x -> x <= y + z).
+  intros ; fourier.
+ apply Sublemma.
+ apply Rlt_le ; apply Sublemma2. rewrite Rabs_Ropp.
+ apply Rlt_le_trans with (r2:=x-lb) ; [| apply RRle_abs] ;
+ apply Rlt_le_trans with (r2:=Rmin (x - lb) (ub - x)) ; [| apply Rmin_l] ;
+ apply Rlt_le_trans with (r2:=Rmin delta' (Rmin (x - lb) (ub - x))).
+ apply Rlt_le_trans with (r2:=delta''). assumption. intuition. apply Rmin_r.
+ apply Rgt_minus. intuition.
+ assert (Sublemma : forall x y z, y <= z - x -> x + y <= z).
+  intros ; fourier.
+ apply Sublemma.
+ apply Rlt_le ; apply Sublemma2.
+ apply Rlt_le_trans with (r2:=ub-x) ; [| apply RRle_abs] ;
+ apply Rlt_le_trans with (r2:=Rmin (x - lb) (ub - x)) ; [| apply Rmin_r] ;
+ apply Rlt_le_trans with (r2:=Rmin delta' (Rmin (x - lb) (ub - x))) ; [| apply Rmin_r] ; assumption.
+ apply Rlt_le_trans with (r2:=delta''). assumption.
+  apply Rle_trans with (r2:=Rmin delta' (Rmin (x - lb) (ub - x))). intuition.
+  apply Rle_trans with (r2:=Rmin (x - lb) (ub - x)). apply Rmin_r. apply Rmin_r.
+         replace ((g (x + h) - g x) / h) with (1/ (h / (g (x + h) - g x))).
+         assert (Hrewr : h = (comp f g ) (x+h) - (comp f g) x).
+          rewrite f_eq_g. rewrite f_eq_g ; unfold id. rewrite Rplus_comm ;
+          unfold Rminus ; rewrite Rplus_assoc ; rewrite Rplus_opp_r. intuition. intuition.    
+ assumption.
+         split ; [|intuition].
+         assert (Sublemma : forall x y z, - z <= y - x -> x <= y + z).
+          intros ; fourier.
+         apply Sublemma ; apply Rlt_le ; apply Sublemma2. rewrite Rabs_Ropp.
+ apply Rlt_le_trans with (r2:=x-lb) ; [| apply RRle_abs] ;
+ apply Rlt_le_trans with (r2:=Rmin (x - lb) (ub - x)) ; [| apply Rmin_l] ;
+ apply Rlt_le_trans with (r2:=Rmin delta' (Rmin (x - lb) (ub - x))) ; [| apply Rmin_r] ; assumption.
+ apply Rgt_minus. intuition.
+ field.
+ split. assumption.
+ intro Hfalse. assert (Hf : g (x+h) = g x) by intuition.
+ assert ((comp f g) (x+h) = (comp f g) x).
+  unfold comp ; rewrite Hf ; intuition.
+ assert (Main : x+h = x).
+ replace (x +h) with (id (x+h)) by intuition.
+ assert (Temp : x = id x) by intuition ; rewrite Temp at 2 ; clear Temp.
+ rewrite <- f_eq_g. rewrite <- f_eq_g. assumption.
+ intuition. assumption.
+ assert (h = 0).
+ apply Rplus_0_r_uniq with (r:=x) ; assumption.
+ apply h_neq ; assumption.
+         replace ((g (x + h) - g x) / h) with (1/ (h / (g (x + h) - g x))).
+         assert (Hrewr : h = (comp f g ) (x+h) - (comp f g) x).
+          rewrite f_eq_g. rewrite f_eq_g. unfold id ; rewrite Rplus_comm ;
+          unfold Rminus ; rewrite Rplus_assoc ; rewrite Rplus_opp_r ; intuition.
+          assumption. assumption.
+         rewrite Hrewr at 1. 
+         unfold comp.
+         replace (g(x+h)) with (g x + (g (x+h) - g(x))) by field.
+         pose (h':=g (x+h) - g x).
+         replace (g (x+h) - g x) with h' by intuition.
+         replace (g x + h' - g x) with h' by field.
+         assert (h'_neq : h' <> 0).
+          unfold h'.
+          intro Hfalse.
+          unfold Rminus in Hfalse ; apply Rminus_diag_uniq in Hfalse.
+          assert (Hfalse' : (comp f g) (x+h) = (comp f g) x).
+           intros ; unfold comp ; rewrite Hfalse ; trivial.
+          rewrite f_eq_g in Hfalse' ; rewrite f_eq_g in Hfalse'.
+          unfold id in Hfalse'.
+          apply Rplus_0_r_uniq in Hfalse'.
+          apply h_neq ; exact Hfalse'. assumption. assumption. assumption.
+         unfold Rdiv at 1 3; rewrite Rmult_1_l ; rewrite Rmult_1_l.
+         apply inv_cont.
+         split.
+          exact h'_neq.
+          rewrite Rminus_0_r. 
+          unfold continuity_pt, continue_in, limit1_in, limit_in in g_cont_pur.
+          elim (g_cont_pur mydelta mydelta_pos).
+          intros delta3 cond3.
+          unfold dist in cond3 ; simpl in cond3 ; unfold R_dist in cond3.
+          unfold h'.
+          assert (mydelta_le_alpha : mydelta <= alpha).
+           unfold mydelta, Rmin ; case (Rle_dec delta alpha).
+           trivial.
+           intro ; intuition.
+          apply Rlt_le_trans with (r2:=mydelta).
+          unfold dist in g_cont ; simpl in g_cont ; unfold R_dist in g_cont ; apply g_cont.
+          split.
+           unfold D_x ; simpl.
+           split.
+            unfold no_cond ; trivial.
+            intro Hfalse ; apply h_neq.
+             apply (Rplus_0_r_uniq x).
+             symmetry ; assumption.
+            replace (x + h - x) with h by field. 
+            apply Rlt_le_trans with (r2:=delta'').
+            assumption ; unfold delta''. intuition.
+            apply Rle_trans with (r2:=mydelta''). apply Req_le. unfold delta''. intuition.
+            apply Rmin_l. assumption.
+            field ; split.
+             assumption.
+             intro Hfalse ; apply h_neq.
+             apply (Rplus_0_r_uniq x).
+             assert (Hfin : (comp f g) (x+h) = (comp f g) x).
+              apply Rminus_diag_uniq in Hfalse.
+              unfold comp.
+              rewrite Hfalse ; reflexivity.
+              rewrite f_eq_g in Hfin. rewrite f_eq_g in Hfin. unfold id in Hfin. exact Hfin.
+              assumption. assumption.
+Qed.
+
+Lemma derivable_pt_recip_interv_prelim0 : forall (f g : R -> R) (lb ub x : R)
+       (Prf : forall a : R, g lb <= a <= g ub -> derivable_pt f a),
+       continuity_pt g x ->
+       lb < ub ->
+       lb < x < ub ->
+       forall Prg_incr : g lb <= g x <= g ub,
+       (forall x0 : R, lb <= x0 <= ub -> comp f g x0 = id x0) ->
+       derive_pt f (g x) (Prf (g x) Prg_incr) <> 0 ->
+       derivable_pt g x.
+Proof.
+intros f g lb ub x Prf g_cont_pt lb_lt_ub x_encad Prg_incr f_eq_g Df_neq.
+unfold derivable_pt, derivable_pt_abs.
+exists (1 / derive_pt f (g x) (Prf (g x) Prg_incr)).
+apply derivable_pt_lim_recip_interv ; assumption.
+Qed.
+
+Lemma derivable_pt_recip_interv_prelim1 :forall (f g:R->R) (lb ub x : R),
+         lb < ub ->
+         f lb < x < f ub ->
+         (forall x : R, f lb <= x -> x <= f ub -> comp f g x = id x) ->
+         (forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
+         (forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y) ->
+         (forall a : R, lb <= a <= ub -> derivable_pt f a) ->
+         derivable_pt f (g x).
+Proof.
+intros f g lb ub x lb_lt_ub x_encad f_eq_g g_ok f_incr f_derivable.
+ apply f_derivable.
+ assert (Left_inv := leftinv_is_rightinv_interv f g lb ub f_incr f_eq_g g_ok).
+ replace lb with ((comp g f) lb).
+ replace ub with ((comp g f) ub).
+ unfold comp.
+ assert (Temp:= f_incr_implies_g_incr_interv f g lb ub lb_lt_ub f_incr f_eq_g g_ok).
+ split ; apply Rlt_le ; apply Temp ; intuition.
+ apply Left_inv ; intuition.
+ apply Left_inv ; intuition.
+Qed.
+
+Lemma derivable_pt_recip_interv : forall (f g:R->R) (lb ub x : R)
+         (lb_lt_ub:lb < ub) (x_encad:f lb < x < f ub)
+         (f_eq_g:forall x : R, f lb <= x -> x <= f ub -> comp f g x = id x)
+         (g_wf:forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub)
+         (f_incr:forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y)
+         (f_derivable:forall a : R, lb <= a <= ub -> derivable_pt f a),
+         derive_pt f (g x)
+              (derivable_pt_recip_interv_prelim1 f g lb ub x lb_lt_ub
+              x_encad f_eq_g g_wf f_incr f_derivable)
+         <> 0 ->
+         derivable_pt g x.
+Proof.
+intros f g lb ub x lb_lt_ub x_encad f_eq_g g_wf f_incr f_derivable Df_neq.
+ assert(g_incr : g (f lb) < g x < g (f ub)).
+  assert (Temp:= f_incr_implies_g_incr_interv f g lb ub lb_lt_ub f_incr f_eq_g g_wf).
+  split ; apply Temp ; intuition.
+  exact (proj1 x_encad). apply Rlt_le ; exact (proj2 x_encad).
+  apply Rlt_le ; exact (proj1 x_encad). exact (proj2 x_encad).
+ assert(g_incr2 :  g (f lb) <= g x <= g (f ub)).
+  split ; apply Rlt_le ; intuition.
+ assert (g_eq_f :=  leftinv_is_rightinv_interv f g lb ub f_incr f_eq_g g_wf).
+ unfold comp, id in g_eq_f.
+ assert (f_derivable2 : forall a : R, g (f lb) <= a <= g (f ub) -> derivable_pt f a).
+  intros a a_encad ; apply f_derivable.
+   rewrite g_eq_f in a_encad ; rewrite g_eq_f in a_encad ; intuition.
+ apply derivable_pt_recip_interv_prelim0 with (f:=f) (lb:=f lb) (ub:=f ub)
+     (Prf:=f_derivable2) (Prg_incr:=g_incr2).
+ apply continuity_pt_recip_interv with (f:=f) (lb:=lb) (ub:=ub) ; intuition.
+ apply derivable_continuous_pt ; apply f_derivable ; intuition.
+ exact (proj1 x_encad). exact (proj2 x_encad).  apply f_incr ; intuition.
+ assumption.
+ intros x0 x0_encad ; apply f_eq_g ; intuition.
+ rewrite pr_nu_var2_interv with (g:=f) (lb:=lb) (ub:=ub) (pr2:=derivable_pt_recip_interv_prelim1 f g lb ub x lb_lt_ub x_encad
+      f_eq_g g_wf f_incr f_derivable) ; [| |rewrite g_eq_f in g_incr ; rewrite g_eq_f in g_incr| ] ; intuition.
+Qed.
+
+(****************************************************)
+(** *   Value of the derivative of the reciprocal function        *)
+(****************************************************)
+
+Lemma derive_pt_recip_interv_prelim0 : forall (f g:R->R) (lb ub x:R)
+       (Prf:derivable_pt f (g x)) (Prg:derivable_pt g x),
+       lb < ub ->
+       lb < x < ub ->
+       (forall x, lb < x < ub -> (comp f g) x = id x) ->
+       derive_pt f (g x) Prf <> 0 ->
+       derive_pt g x Prg = 1 / (derive_pt f (g x) Prf).
+Proof.
+intros f g lb ub x Prf Prg lb_lt_ub x_encad local_recip Df_neq.
+ replace (derive_pt g x Prg) with
+  ((derive_pt g x Prg) * (derive_pt f (g x) Prf) * / (derive_pt f (g x) Prf)).
+ unfold Rdiv.
+ rewrite (Rmult_comm _ (/ derive_pt f (g x) Prf)).
+ rewrite (Rmult_comm _ (/ derive_pt f (g x) Prf)). 
+ apply Rmult_eq_compat_l. 
+ rewrite Rmult_comm.
+ rewrite <- derive_pt_comp.
+ assert (x_encad2 : lb <= x <= ub) by intuition.
+ rewrite pr_nu_var2_interv with (g:=id) (pr2:= derivable_pt_id_interv lb ub x x_encad2) (lb:=lb) (ub:=ub) ; [reg| | |] ; assumption.
+ rewrite Rmult_assoc, Rinv_r.
+ intuition.
+ assumption.
+Qed.
+
+Lemma derive_pt_recip_interv_prelim1_0 : forall (f g:R->R) (lb ub x:R), 
+       lb < ub ->
+       f lb < x < f ub ->
+       (forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y) ->
+       (forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
+       (forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x) ->
+       lb < g x < ub.
+Proof.
+intros f g lb ub x lb_lt_ub x_encad f_incr g_wf f_eq_g.
+ assert (Temp:= f_incr_implies_g_incr_interv f g lb ub lb_lt_ub f_incr f_eq_g g_wf).
+ assert (Left_inv := leftinv_is_rightinv_interv f g lb ub f_incr f_eq_g g_wf).
+ unfold comp, id in Left_inv.
+ split ; [rewrite <- Left_inv with (x:=lb) | rewrite <- Left_inv ].
+ apply Temp ; intuition.
+ intuition.
+ apply Temp ; intuition.
+ intuition.
+Qed.
+
+Lemma derive_pt_recip_interv_prelim1_1 : forall (f g:R->R) (lb ub x:R), 
+       lb < ub ->
+       f lb < x < f ub ->
+       (forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y) ->
+       (forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
+       (forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x) ->
+       lb <= g x <= ub.
+Proof.
+intros f g lb ub x lb_lt_ub x_encad f_incr g_wf f_eq_g.
+ assert (Temp := derive_pt_recip_interv_prelim1_0 f g lb ub x lb_lt_ub x_encad f_incr g_wf f_eq_g).
+ split ; apply Rlt_le ; intuition.
+Qed.
+
+Lemma derive_pt_recip_interv : forall (f g:R->R) (lb ub x:R)
+       (lb_lt_ub:lb < ub) (x_encad:f lb < x < f ub)
+       (f_incr:forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y)
+       (g_wf:forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub)
+       (Prf:forall a : R, lb <= a <= ub -> derivable_pt f a)
+       (f_eq_g:forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x)
+       (Df_neq:derive_pt f (g x) (derivable_pt_recip_interv_prelim1 f g lb ub x
+                 lb_lt_ub x_encad f_eq_g g_wf f_incr Prf) <> 0),
+       derive_pt g x (derivable_pt_recip_interv f g lb ub x lb_lt_ub x_encad f_eq_g
+                 g_wf f_incr Prf Df_neq)
+       =
+       1 / (derive_pt f (g x) (Prf (g x) (derive_pt_recip_interv_prelim1_1 f g lb ub x
+       lb_lt_ub x_encad f_incr g_wf f_eq_g))).
+Proof.
+intros.
+ assert(g_incr := (derive_pt_recip_interv_prelim1_1 f g lb ub x lb_lt_ub
+        x_encad f_incr g_wf f_eq_g)).
+ apply derive_pt_recip_interv_prelim0 with (lb:=f lb) (ub:=f ub) ;
+ [intuition |assumption | intuition |].
+ intro Hfalse ; apply Df_neq.  rewrite pr_nu_var2_interv with (g:=f) (lb:=lb) (ub:=ub)
+        (pr2:= (Prf (g x) (derive_pt_recip_interv_prelim1_1 f g lb ub x lb_lt_ub x_encad
+                 f_incr g_wf f_eq_g))) ;
+ [intuition | intuition | | intuition].
+ exact (derive_pt_recip_interv_prelim1_0 f g lb ub x lb_lt_ub x_encad f_incr g_wf f_eq_g).
+Qed.
+  
+(****************************************************)
+(** * Existence of the derivative of a function which is the limit of a sequence of functions *)
+(****************************************************)
+
+(* begin hide *)
+Lemma ub_lt_2_pos : forall x ub lb, lb < x -> x < ub -> 0 < (ub-lb)/2.
+Proof.
+intros x ub lb lb_lt_x x_lt_ub.
+ assert (T : 0 < ub - lb).
+  fourier.
+ unfold Rdiv ; apply Rlt_mult_inv_pos ; intuition.
+Qed.
+
+Definition mkposreal_lb_ub (x lb ub:R) (lb_lt_x:lb<x) (x_lt_ub:x<ub) : posreal.
+ apply (mkposreal ((ub-lb)/2) (ub_lt_2_pos x ub lb lb_lt_x x_lt_ub)).
+Defined.
+(* end hide *)
+
+Definition boule_of_interval x y (h : x < y) :
+  {c :R & {r : posreal | c - r = x /\ c + r = y}}.
+exists ((x + y)/2).
+assert (radius : 0 < (y - x)/2).
+ unfold Rdiv; apply Rmult_lt_0_compat; fourier.
+ exists (mkposreal _ radius).
+ simpl; split; unfold Rdiv; field.
+Qed.
+
+Definition boule_in_interval x y z (h : x < z < y) :
+  {c : R & {r | Boule c r z /\  x < c - r /\ c + r < y}}.
+Proof.
+assert (cmp : x * /2 + z * /2 < z * /2 + y * /2).
+destruct h as [h1 h2]; fourier.
+destruct (boule_of_interval _ _ cmp) as [c [r [P1 P2]]].
+exists c, r; split.
+ destruct h; unfold Boule; simpl; apply Rabs_def1; fourier.
+destruct h; split; fourier.
+Qed.
+
+Lemma Ball_in_inter : forall c1 c2 r1 r2 x,
+  Boule c1 r1 x -> Boule c2 r2 x ->
+  {r3 : posreal | forall y, Boule x r3 y -> Boule c1 r1 y /\ Boule c2 r2 y}.
+intros c1 c2 [r1 r1p] [r2 r2p] x; unfold Boule; simpl; intros in1 in2.
+assert (Rmax (c1 - r1)(c2 - r2) < x).
+ apply Rmax_lub_lt;[revert in1 | revert in2]; intros h;
+  apply Rabs_def2 in h; destruct h; fourier.
+assert (x < Rmin (c1 + r1) (c2 + r2)).
+ apply Rmin_glb_lt;[revert in1 | revert in2]; intros h;
+  apply Rabs_def2 in h; destruct h; fourier.
+assert (t: 0 < Rmin (x - Rmax (c1 - r1) (c2 - r2)) 
+              (Rmin (c1 + r1) (c2 + r2) - x)).
+ apply Rmin_glb_lt; fourier.
+exists (mkposreal _ t).
+apply Rabs_def2 in in1; destruct in1.
+apply Rabs_def2 in in2; destruct in2.
+assert (c1 - r1 <= Rmax (c1 - r1) (c2 - r2)) by apply Rmax_l.
+assert (c2 - r2 <= Rmax (c1 - r1) (c2 - r2)) by apply Rmax_r.
+assert (Rmin (c1 + r1) (c2 + r2) <= c1 + r1) by apply Rmin_l.
+assert (Rmin (c1 + r1) (c2 + r2) <= c2 + r2) by apply Rmin_r.
+assert (Rmin (x - Rmax (c1 - r1) (c2 - r2)) 
+         (Rmin (c1 + r1) (c2 + r2) - x) <= x - Rmax (c1 - r1) (c2 - r2))
+ by apply Rmin_l.
+assert (Rmin (x - Rmax (c1 - r1) (c2 - r2)) 
+         (Rmin (c1 + r1) (c2 + r2) - x) <= Rmin (c1 + r1) (c2 + r2) - x)
+ by apply Rmin_r.
+simpl.
+intros y h; apply Rabs_def2 in h; destruct h;split; apply Rabs_def1; fourier.
+Qed.
+
+Lemma Boule_center : forall x r, Boule x r x.
+Proof.
+intros x [r rpos]; unfold Boule, Rminus; simpl; rewrite Rplus_opp_r.
+rewrite Rabs_pos_eq;[assumption | apply Rle_refl].
+Qed.
+
+Lemma derivable_pt_lim_CVU : forall (fn fn':nat -> R -> R) (f g:R->R)
+      (x:R) c r, Boule c r x ->
+      (forall y n, Boule c r y -> derivable_pt_lim (fn n) y (fn' n y)) ->
+      (forall y, Boule c r y -> Un_cv (fun n => fn n y) (f y)) ->
+      (CVU fn' g c r) ->
+      (forall y, Boule c r y -> continuity_pt g y) ->
+      derivable_pt_lim f x (g x).
+Proof.
+intros fn fn' f g x c' r xinb Dfn_eq_fn' fn_CV_f fn'_CVU_g g_cont eps eps_pos.
+assert (eps_8_pos : 0 < eps / 8) by fourier.
+elim (g_cont x xinb _ eps_8_pos) ; clear g_cont ;
+intros delta1 (delta1_pos, g_cont).
+destruct (Ball_in_inter _ _ _ _ _ xinb
+   (Boule_center x (mkposreal _ delta1_pos)))
+   as [delta Pdelta].
+exists delta; intros h hpos hinbdelta.
+assert (eps'_pos : 0 < (Rabs h) * eps / 4).
+ unfold Rdiv ; rewrite Rmult_assoc ; apply Rmult_lt_0_compat.
+ apply Rabs_pos_lt ; assumption.
+fourier.
+destruct (fn_CV_f x xinb ((Rabs h) * eps / 4) eps'_pos) as [N2 fnx_CV_fx].
+assert (xhinbxdelta : Boule x delta (x + h)).
+ clear -hinbdelta; apply Rabs_def2 in hinbdelta; unfold Boule; simpl.
+ destruct hinbdelta; apply Rabs_def1; fourier.
+assert (t : Boule c' r (x + h)).
+ apply Pdelta in xhinbxdelta; tauto.
+destruct (fn_CV_f (x+h) t ((Rabs h) * eps / 4) eps'_pos) as [N1 fnxh_CV_fxh].
+clear fn_CV_f t.
+destruct (fn'_CVU_g (eps/8) eps_8_pos) as [N3 fn'c_CVU_gc].
+pose (N := ((N1 + N2) + N3)%nat).
+assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn N x - h * (g x))) < (Rabs h)*eps).
+ apply Rle_lt_trans with (Rabs (f (x + h) - fn N (x + h) - (f x - fn N x)) +  Rabs ((fn N (x + h) - fn N x - h * g x))).
+  solve[apply Rabs_triang].
+ apply Rle_lt_trans with (Rabs (f (x + h) - fn N (x + h)) + Rabs (- (f x - fn N x)) + Rabs (fn N (x + h) - fn N x - h * g x)).
+  solve[apply Rplus_le_compat_r ; apply Rabs_triang].
+ rewrite Rabs_Ropp.
+ case (Rlt_le_dec h 0) ; intro sgn_h.
+  assert (pr1 : forall c : R, x + h < c < x -> derivable_pt (fn N) c).
+   intros c c_encad ; unfold derivable_pt.
+   exists (fn' N c) ; apply Dfn_eq_fn'.
+   assert (t : Boule x delta c).
+    apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta; destruct c_encad.
+    apply Rabs_def2 in xinb; apply Rabs_def1; fourier.
+   apply Pdelta in t; tauto.
+  assert (pr2 : forall c : R, x + h < c < x -> derivable_pt id c).
+   solve[intros; apply derivable_id].
+  assert (xh_x : x+h < x) by fourier.
+  assert (pr3 : forall c : R, x + h <= c <= x -> continuity_pt (fn N) c).
+   intros c c_encad ; apply derivable_continuous_pt.
+   exists (fn' N c) ; apply Dfn_eq_fn' ; intuition.
+   assert (t : Boule x delta c).
+    apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta.
+    apply Rabs_def2 in xinb; apply Rabs_def1; fourier.
+   apply Pdelta in t; tauto.
+  assert (pr4 : forall c : R, x + h <= c <= x -> continuity_pt id c).
+   solve[intros; apply derivable_continuous ; apply derivable_id].
+  destruct (MVT (fn N) id (x+h) x pr1 pr2 xh_x pr3 pr4) as [c [P Hc]].
+  assert (Hc' : h * derive_pt (fn N) c (pr1 c P) = (fn N (x+h) - fn N x)).
+   apply Rmult_eq_reg_l with (-1).
+    replace (-1 * (h * derive_pt (fn N) c (pr1 c P))) with (-h * derive_pt (fn N) c (pr1 c P)) by field.
+    replace (-1 * (fn N (x + h) - fn N x)) with (- (fn N (x + h) - fn N x)) by field.
+    replace (-h) with (id x - id (x + h)) by (unfold id; field).
+    rewrite <- Rmult_1_r ; replace 1 with (derive_pt id c (pr2 c P)) by reg.
+    replace (- (fn N (x + h) - fn N x)) with (fn N x - fn N (x + h)) by field.
+    assumption.
+   solve[apply Rlt_not_eq ; intuition].
+  rewrite <- Hc'; clear Hc Hc'.
+  replace (derive_pt (fn N) c (pr1 c P)) with (fn' N c).
+  replace (h * fn' N c - h * g x) with (h * (fn' N c - g x)) by field.
+   rewrite Rabs_mult.
+   apply Rlt_trans with (Rabs h * eps / 4 + Rabs (f x - fn N x) + Rabs h * Rabs (fn' N c - g x)).
+    apply Rplus_lt_compat_r ; apply Rplus_lt_compat_r ; unfold R_dist in fnxh_CV_fxh ;
+ rewrite Rabs_minus_sym ; apply fnxh_CV_fxh.
+   unfold N; omega.
+   apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g x)).
+    apply Rplus_lt_compat_r ; apply Rplus_lt_compat_l.
+    unfold R_dist in fnx_CV_fx ; rewrite Rabs_minus_sym ; apply fnx_CV_fx.
+    unfold N ; omega.
+   replace (fn' N c - g x)  with ((fn' N c - g c) +  (g c - g x)) by field.
+   apply Rle_lt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 +
+          Rabs h * Rabs (fn' N c - g c) + Rabs h * Rabs (g c - g x)).
+    rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite Rplus_assoc ;
+    apply Rplus_le_compat_l ; apply Rplus_le_compat_l ;
+    rewrite <- Rmult_plus_distr_l ; apply Rmult_le_compat_l. 
+     solve[apply Rabs_pos].
+    solve[apply Rabs_triang].
+   apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 +
+          Rabs h * (eps / 8) + Rabs h * Rabs (g c - g x)).
+    apply Rplus_lt_compat_r; apply Rplus_lt_compat_l; apply Rmult_lt_compat_l.
+     apply Rabs_pos_lt ; assumption.
+    rewrite Rabs_minus_sym ; apply fn'c_CVU_gc.
+     unfold N ; omega.
+    assert (t : Boule x delta c).
+     destruct P.
+     apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta.
+     apply Rabs_def2 in xinb; apply Rabs_def1; fourier.
+    apply Pdelta in t; tauto.
+   apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * (eps / 8) +
+         Rabs h * (eps / 8)).
+    rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite Rplus_assoc ;
+    apply Rplus_lt_compat_l ; apply Rplus_lt_compat_l ; rewrite <- Rmult_plus_distr_l ;
+    rewrite <- Rmult_plus_distr_l ; apply Rmult_lt_compat_l.
+     apply Rabs_pos_lt ; assumption.
+     apply Rplus_lt_compat_l ; simpl in g_cont ; apply g_cont ; split ; [unfold D_x ; split |].
+      solve[unfold no_cond ; intuition].
+     apply Rgt_not_eq ; exact (proj2 P).
+    apply Rlt_trans with (Rabs h).
+     apply Rabs_def1. 
+      apply Rlt_trans with 0.
+       destruct P; fourier.
+      apply Rabs_pos_lt ; assumption.
+     rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_involutive;[ | fourier]. 
+     destruct P; fourier.
+    clear -Pdelta xhinbxdelta.
+    apply Pdelta in xhinbxdelta; destruct xhinbxdelta as [_ P'].
+    apply Rabs_def2 in P'; simpl in P'; destruct P';
+    apply Rabs_def1; fourier.
+   rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite <- Rmult_plus_distr_l.
+   replace (Rabs h * eps / 4 + (Rabs h * eps / 4 + Rabs h * (eps / 8 + eps / 8))) with
+      (Rabs h * (eps / 4 + eps / 4 + eps / 8 + eps / 8)) by field.
+   apply Rmult_lt_compat_l. 
+    apply Rabs_pos_lt ; assumption.
+   fourier.
+  assert (H := pr1 c P) ; elim H ; clear H ; intros l Hl.
+  assert (Temp : l = fn' N c).
+   assert (bc'rc : Boule c' r c).
+    assert (t : Boule x delta c).
+     clear - xhinbxdelta P.
+     destruct P; apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta.
+     apply Rabs_def1; fourier.
+    apply Pdelta in t; tauto.
+   assert (Hl' := Dfn_eq_fn' c N bc'rc).
+   unfold derivable_pt_abs in Hl; clear -Hl Hl'.
+   apply uniqueness_limite with (f:= fn N) (x:=c) ; assumption.
+  rewrite <- Temp.
+  assert (Hl' : derivable_pt (fn N) c).
+  exists l ; apply Hl.
+  rewrite pr_nu_var with (g:= fn N) (pr2:=Hl').
+   elim Hl' ; clear Hl' ; intros l' Hl'.
+   assert (Main : l = l').
+    apply uniqueness_limite with (f:= fn N) (x:=c) ; assumption.
+   rewrite Main ; reflexivity.
+  reflexivity.
+ assert (h_pos : h > 0).
+  case sgn_h ; intro Hyp.
+  assumption.
+  apply False_ind ; apply hpos ; symmetry ; assumption.
+ clear sgn_h.
+ assert (pr1 : forall c : R, x < c < x + h -> derivable_pt (fn N) c).
+  intros c c_encad ; unfold derivable_pt.
+  exists (fn' N c) ; apply Dfn_eq_fn'.
+  assert (t : Boule x delta c).
+   apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta; destruct c_encad.
+   apply Rabs_def2 in xinb; apply Rabs_def1; fourier.
+  apply Pdelta in t; tauto.
+  assert (pr2 : forall c : R, x < c < x + h -> derivable_pt id c).
+   solve[intros; apply derivable_id].
+  assert (xh_x : x < x + h) by fourier.
+  assert (pr3 : forall c : R, x <= c <= x + h -> continuity_pt (fn N) c).
+   intros c c_encad ; apply derivable_continuous_pt.
+   exists (fn' N c) ; apply Dfn_eq_fn' ; intuition.
+   assert (t : Boule x delta c).
+    apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta.
+    apply Rabs_def2 in xinb; apply Rabs_def1; fourier.
+   apply Pdelta in t; tauto.
+  assert (pr4 : forall c : R, x <= c <= x + h -> continuity_pt id c).
+   solve[intros; apply derivable_continuous ; apply derivable_id].
+  destruct (MVT (fn N) id x (x+h) pr1 pr2 xh_x pr3 pr4) as [c [P Hc]].
+  assert (Hc' : h * derive_pt (fn N) c (pr1 c P) = fn N (x+h) - fn N x).
+    pattern h at 1; replace h with (id (x + h) - id x) by (unfold id; field).
+    rewrite <- Rmult_1_r ; replace 1 with (derive_pt id c (pr2 c P)) by reg.
+    assumption.
+  rewrite <- Hc'; clear Hc Hc'.
+  replace (derive_pt (fn N) c (pr1 c P)) with (fn' N c).
+  replace (h * fn' N c - h * g x) with (h * (fn' N c - g x)) by field.
+   rewrite Rabs_mult.
+   apply Rlt_trans with (Rabs h * eps / 4 + Rabs (f x - fn N x) + Rabs h * Rabs (fn' N c - g x)).
+    apply Rplus_lt_compat_r ; apply Rplus_lt_compat_r ; unfold R_dist in fnxh_CV_fxh ;
+ rewrite Rabs_minus_sym ; apply fnxh_CV_fxh.
+   unfold N; omega.
+   apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g x)).
+    apply Rplus_lt_compat_r ; apply Rplus_lt_compat_l.
+    unfold R_dist in fnx_CV_fx ; rewrite Rabs_minus_sym ; apply fnx_CV_fx.
+    unfold N ; omega.
+   replace (fn' N c - g x)  with ((fn' N c - g c) +  (g c - g x)) by field.
+   apply Rle_lt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 +
+          Rabs h * Rabs (fn' N c - g c) + Rabs h * Rabs (g c - g x)).
+    rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite Rplus_assoc ;
+    apply Rplus_le_compat_l ; apply Rplus_le_compat_l ;
+    rewrite <- Rmult_plus_distr_l ; apply Rmult_le_compat_l. 
+     solve[apply Rabs_pos].
+    solve[apply Rabs_triang].
+   apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 +
+          Rabs h * (eps / 8) + Rabs h * Rabs (g c - g x)).
+    apply Rplus_lt_compat_r; apply Rplus_lt_compat_l; apply Rmult_lt_compat_l.
+     apply Rabs_pos_lt ; assumption.
+    rewrite Rabs_minus_sym ; apply fn'c_CVU_gc.
+     unfold N ; omega.
+    assert (t : Boule x delta c).
+     destruct P.
+    apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta.
+    apply Rabs_def2 in xinb; apply Rabs_def1; fourier.
+   apply Pdelta in t; tauto.
+  apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * (eps / 8) +
+         Rabs h * (eps / 8)).
+   rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite Rplus_assoc ;
+    apply Rplus_lt_compat_l ; apply Rplus_lt_compat_l ; rewrite <- Rmult_plus_distr_l ;
+   rewrite <- Rmult_plus_distr_l ; apply Rmult_lt_compat_l.
+    apply Rabs_pos_lt ; assumption.
+   apply Rplus_lt_compat_l ; simpl in g_cont ; apply g_cont ; split ; [unfold D_x ; split |].
+     solve[unfold no_cond ; intuition].
+    apply Rlt_not_eq ; exact (proj1 P).
+   apply Rlt_trans with (Rabs h).
+    apply Rabs_def1.
+     destruct P; rewrite Rabs_pos_eq;fourier.
+    apply Rle_lt_trans with 0.
+     assert (t := Rabs_pos h); clear -t; fourier.
+    clear -P; destruct P; fourier.
+   clear -Pdelta xhinbxdelta.
+   apply Pdelta in xhinbxdelta; destruct xhinbxdelta as [_ P'].
+   apply Rabs_def2 in P'; simpl in P'; destruct P';
+    apply Rabs_def1; fourier.
+  rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite <- Rmult_plus_distr_l.
+  replace (Rabs h * eps / 4 + (Rabs h * eps / 4 + Rabs h * (eps / 8 + eps / 8))) with
+      (Rabs h * (eps / 4 + eps / 4 + eps / 8 + eps / 8)) by field.
+  apply Rmult_lt_compat_l. 
+   apply Rabs_pos_lt ; assumption.
+  fourier.
+ assert (H := pr1 c P) ; elim H ; clear H ; intros l Hl.
+ assert (Temp : l = fn' N c).
+  assert (bc'rc : Boule c' r c).
+   assert (t : Boule x delta c).
+    clear - xhinbxdelta P.
+    destruct P; apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta.
+    apply Rabs_def1; fourier.
+   apply Pdelta in t; tauto.
+  assert (Hl' := Dfn_eq_fn' c N bc'rc).
+  unfold derivable_pt_abs in Hl; clear -Hl Hl'.
+  apply uniqueness_limite with (f:= fn N) (x:=c) ; assumption.
+ rewrite <- Temp.
+ assert (Hl' : derivable_pt (fn N) c).
+ exists l ; apply Hl.
+ rewrite pr_nu_var with (g:= fn N) (pr2:=Hl').
+  elim Hl' ; clear Hl' ; intros l' Hl'.
+  assert (Main : l = l').
+   apply uniqueness_limite with (f:= fn N) (x:=c) ; assumption.
+  rewrite Main ; reflexivity.
+ reflexivity.
+ replace ((f (x + h) - f x) / h - g x) with ((/h) * ((f (x + h) - f x) - h * g x)). 
+ rewrite Rabs_mult ; rewrite Rabs_Rinv.
+ replace eps with (/ Rabs h * (Rabs h * eps)).
+ apply Rmult_lt_compat_l.
+ apply Rinv_0_lt_compat ; apply Rabs_pos_lt ; assumption.
+ replace (f (x + h) - f x - h * g x) with (f (x + h) - fn N (x + h) - (f x - fn N x) +
+          (fn N (x + h) - fn N x - h * g x)) by field.
+ assumption.
+ field ; apply Rgt_not_eq ; apply Rabs_pos_lt ; assumption.
+ assumption.
+ field. assumption.
+Qed.
\ No newline at end of file
diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v
new file mode 100644
index 000000000..4c6bc6fc2
--- /dev/null
+++ b/theories/Reals/Ratan.v
@@ -0,0 +1,1602 @@
+Require Import Fourier.
+Require Import Rbase.
+Require Import PSeries_reg.
+Require Import Rtrigo.
+Require Import Ranalysis.
+Require Import Rfunctions.
+Require Import AltSeries.
+Require Import Rseries.
+Require Import SeqProp.
+Require Import Ranalysis5.
+Require Import SeqSeries.
+Require Import PartSum.
+
+Open Local Scope R_scope.
+
+(** Tools *)
+
+Lemma Ropp_div : forall x y, -x/y = -(x/y).
+Proof.
+intros x y; unfold Rdiv; rewrite <-Ropp_mult_distr_l_reverse; reflexivity.
+Qed.
+
+Definition pos_half_prf : 0 < /2.
+Proof. fourier. Qed.
+
+Definition pos_half := mkposreal (/2) pos_half_prf.
+
+Lemma Boule_half_to_interval :
+  forall x , Boule (/2) pos_half x -> 0 <= x <= 1.
+Proof.
+unfold Boule, pos_half; simpl.
+intros x b; apply Rabs_def2 in b; destruct b; split; fourier.
+Qed.
+
+Lemma Boule_lt : forall c r x, Boule c r x -> Rabs x < Rabs c + r.
+Proof.
+unfold Boule; intros c r x h.
+apply Rabs_def2 in h; destruct h; apply Rabs_def1;
+ (destruct (Rle_lt_dec 0 c);[rewrite Rabs_pos_eq; fourier | 
+    rewrite <- Rabs_Ropp, Rabs_pos_eq; fourier]).
+Qed.
+
+(* The following lemma does not belong here. *)
+Lemma Un_cv_ext :
+  forall un vn, (forall n, un n = vn n) ->
+  forall l, Un_cv un l -> Un_cv vn l.
+Proof.
+intros un vn quv l P eps ep; destruct (P eps ep) as [N Pn]; exists N.
+intro n; rewrite <- quv; apply Pn.
+Qed.
+
+(* The following two lemmas are general purposes about alternated series.
+  They do not belong here. *)
+Lemma Alt_first_term_bound :forall f l N n,
+   Un_decreasing f -> Un_cv f 0 ->
+   Un_cv (sum_f_R0 (tg_alt f)) l ->
+   (N <= n)%nat ->
+   R_dist (sum_f_R0 (tg_alt f) n) l <= f N.
+Proof.
+intros f l.
+assert (WLOG :
+   forall n P, (forall k, (0 < k)%nat -> P k) ->
+         ((forall k, (0 < k)%nat -> P k) -> P 0%nat) -> P n).
+clear.
+intros [ | n] P Hs Ho;[solve[apply Ho, Hs] | apply Hs; auto with arith].
+intros N; pattern N; apply WLOG; clear N.
+intros [ | N] Npos n decr to0 cv nN.
+  clear -Npos; elimtype False; omega.
+ assert (decr' : Un_decreasing (fun i => f (S N + i)%nat)).
+  intros k; replace (S N+S k)%nat with (S (S N+k)) by ring.
+  apply (decr (S N + k)%nat).
+ assert (to' : Un_cv (fun i => f (S N + i)%nat) 0).
+  intros eps ep; destruct (to0 eps ep) as [M PM].
+  exists M; intros k kM; apply PM; omega.
+ assert (cv' : Un_cv
+         (sum_f_R0 (tg_alt (fun i => ((-1) ^ S N * f(S N + i)%nat))))
+             (l - sum_f_R0 (tg_alt f) N)).
+  intros eps ep; destruct (cv eps ep) as [M PM]; exists M.
+  intros n' nM. 
+  match goal with |- ?C => set (U := C) end.
+  assert (nM' : (n' + S N >= M)%nat) by omega.
+   generalize (PM _ nM'); unfold R_dist.
+  rewrite (tech2 (tg_alt f) N (n' + S N)).
+  assert (t : forall a b c, (a + b) - c = b - (c - a)) by (intros; ring).
+  rewrite t; clear t; unfold U, R_dist; clear U.
+  replace (n' + S N - S N)%nat with n' by omega.
+  rewrite <- (sum_eq (tg_alt (fun i => (-1) ^ S N * f(S N + i)%nat))).
+   tauto.
+   intros i _; unfold tg_alt.
+   rewrite <- Rmult_assoc, <- pow_add, !(plus_comm i); reflexivity.
+  omega.
+  assert (cv'' : Un_cv (sum_f_R0 (tg_alt (fun i => f (S N + i)%nat)))
+                   ((-1) ^ S N * (l - sum_f_R0 (tg_alt f) N))).
+  apply (Un_cv_ext (fun n => (-1) ^ S N * 
+            sum_f_R0 (tg_alt (fun i : nat => (-1) ^ S N * f (S N + i)%nat)) n)).
+   intros n0; rewrite scal_sum; apply sum_eq; intros i _.
+   unfold tg_alt; ring_simplify; replace (((-1) ^ S N) ^ 2) with 1.
+    ring.
+   rewrite <- pow_mult, mult_comm, pow_mult; replace ((-1) ^2) with 1 by ring.
+   rewrite pow1; reflexivity.
+  apply CV_mult.
+   solve[intros eps ep; exists 0%nat; intros; rewrite R_dist_eq; auto].
+  assumption.
+ destruct (even_odd_cor N) as [p [Neven | Nodd]].
+  rewrite Neven; destruct (alternated_series_ineq _ _ p decr to0 cv) as [B C].
+  case (even_odd_cor n) as [p' [neven | nodd]].
+   rewrite neven.
+   destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E].
+   unfold R_dist; rewrite Rabs_pos_eq;[ | fourier].
+   assert (dist : (p <= p')%nat) by omega.
+   assert (t := decreasing_prop _ _ _ (CV_ALT_step1 f decr) dist).
+   apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * p) - l).
+    unfold Rminus; apply Rplus_le_compat_r; exact t.
+   match goal with _ : ?a <= l, _ : l <= ?b |- _ => 
+    replace (f (S (2 * p))) with (b - a) by
+     (rewrite tech5; unfold tg_alt; rewrite pow_1_odd; ring); fourier
+   end.
+  rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E].
+   unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_minus_distr;
+     [ | fourier].
+   assert (dist : (p <= p')%nat) by omega.
+   apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))).
+    unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar.
+    solve[apply Rge_le, (growing_prop _ _ _ (CV_ALT_step0 f decr) dist)].
+   unfold Rminus; rewrite tech5, Ropp_plus_distr, <- Rplus_assoc.
+   unfold tg_alt at 2; rewrite pow_1_odd, Ropp_mult_distr_l_reverse; fourier.
+ rewrite Nodd; destruct (alternated_series_ineq _ _ p decr to0 cv) as [B _].
+ destruct (alternated_series_ineq _ _ (S p) decr to0 cv) as [_ C].
+ assert (keep : (2 * S p = S (S ( 2 * p)))%nat) by ring.
+ case (even_odd_cor n) as [p' [neven | nodd]].
+   rewrite neven;
+   destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E].
+   unfold R_dist; rewrite Rabs_pos_eq;[ | fourier].
+   assert (dist : (S p < S p')%nat) by omega.
+   apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * S p) - l).
+   unfold Rminus; apply Rplus_le_compat_r,
+     (decreasing_prop _ _ _ (CV_ALT_step1 f decr)).
+   omega.
+  rewrite keep, tech5; unfold tg_alt at 2; rewrite <- keep, pow_1_even.
+  fourier.
+ rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E].
+ unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq;[ | fourier].
+ rewrite Ropp_minus_distr.
+ apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))).
+  unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar, Rge_le,
+   (growing_prop _ _ _ (CV_ALT_step0 f decr)); omega.
+ generalize C; rewrite keep, tech5; unfold tg_alt.
+ rewrite <- keep, pow_1_even.
+ assert (t : forall a b c, a <= b + 1 * c -> a - b <= c) by (intros; fourier).
+ solve[apply t].
+clear WLOG; intros Hyp [ | n] decr to0 cv _.
+ generalize (alternated_series_ineq f l 0 decr to0 cv).
+ unfold R_dist, tg_alt; simpl; rewrite !Rmult_1_l, !Rmult_1_r.
+ assert (f 1%nat <= f 0%nat) by apply decr.
+ rewrite Ropp_mult_distr_l_reverse.
+ intros [A B]; rewrite Rabs_pos_eq; fourier.
+apply Rle_trans with (f 1%nat).
+ apply (Hyp 1%nat (le_n 1) (S n) decr to0 cv).
+ omega.
+solve[apply decr].
+Qed.
+
+Lemma Alt_CVU : forall (f : nat -> R -> R) g h c r,
+   (forall x, Boule c r x ->Un_decreasing (fun n => f n x)) -> 
+   (forall x, Boule c r x -> Un_cv (fun n => f n x) 0) ->
+   (forall x, Boule c r x -> 
+       Un_cv (sum_f_R0 (tg_alt  (fun i => f i x))) (g x)) ->
+   (forall x n, Boule c r x -> f n x <= h n) ->
+   (Un_cv h 0) ->
+   CVU (fun N x => sum_f_R0 (tg_alt (fun i => f i x)) N) g c r.
+Proof.
+intros f g h c r decr to0 to_g bound bound0 eps ep.  
+assert (ep' : 0 <eps/2) by fourier.
+destruct (bound0 _ ep) as [N Pn]; exists N.
+intros n y nN dy.
+rewrite <- Rabs_Ropp, Ropp_minus_distr; apply Rle_lt_trans with (f n y).
+ solve[apply (Alt_first_term_bound (fun i => f i y) (g y) n n); auto].
+apply Rle_lt_trans with (h n).
+ apply bound; assumption.
+clear - nN Pn.
+generalize (Pn _ nN); unfold R_dist; rewrite Rminus_0_r; intros t.
+apply Rabs_def2 in t; tauto.
+Qed.
+
+(* The following lemmas are general purpose lemmas about squares. 
+  They do not belong here *)
+
+Lemma pow2_ge_0 : forall x, 0 <= x ^ 2.
+Proof.
+intros x; destruct (Rle_lt_dec 0 x).
+ replace (x ^ 2) with (x * x) by field.
+ apply Rmult_le_pos; assumption.
+ replace (x ^ 2) with ((-x) * (-x)) by field.
+apply Rmult_le_pos; fourier.
+Qed.
+
+Lemma pow2_abs : forall x,  Rabs x ^ 2 = x ^ 2.
+Proof.
+intros x; destruct (Rle_lt_dec 0 x).
+ rewrite Rabs_pos_eq;[field | assumption].
+rewrite <- Rabs_Ropp, Rabs_pos_eq;[field | fourier].
+Qed.
+
+(** * Properties of tangent *)
+
+Lemma derivable_pt_tan : forall x, -PI/2 < x < PI/2 -> derivable_pt tan x.
+Proof.
+intros x xint.
+ unfold derivable_pt, tan. 
+ apply derivable_pt_div ; [reg | reg | ].
+ apply Rgt_not_eq.
+ unfold Rgt ; apply cos_gt_0;
+  [unfold Rdiv; rewrite <- Ropp_mult_distr_l_reverse; fold (-PI/2) |];tauto.
+Qed.
+
+Lemma derive_pt_tan : forall (x:R),
+ forall (Pr1: -PI/2 < x < PI/2),
+ derive_pt tan x (derivable_pt_tan x Pr1) = 1 + (tan x)^2.
+Proof.
+intros x pr.
+assert (cos x <> 0).
+ apply Rgt_not_eq, cos_gt_0; rewrite <- ?Ropp_div; tauto.
+unfold tan; reg; unfold pow, Rsqr; field; assumption.
+Qed.
+
+(** Proof that tangent is a bijection *)
+(* to be removed? *)
+
+Lemma derive_increasing_interv :
+  forall (a b:R) (f:R -> R),
+    a < b ->
+    forall (pr:forall x, a < x < b -> derivable_pt f x),
+    (forall t:R, forall (t_encad : a < t < b), 0 < derive_pt f t (pr t t_encad)) ->
+    forall x y:R, a < x < b -> a < y < b -> x < y -> f x < f y.
+Proof.
+intros a b f a_lt_b pr Df_gt_0 x y x_encad y_encad x_lt_y.
+ assert (derivable_id_interv : forall c : R, x < c < y -> derivable_pt id c).
+  intros ; apply derivable_pt_id.
+ assert (derivable_f_interv :  forall c : R, x < c < y -> derivable_pt f c).
+  intros c c_encad. apply pr. split.
+  apply Rlt_trans with (r2:=x) ; [exact (proj1 x_encad) | exact (proj1 c_encad)].
+  apply Rlt_trans with (r2:=y) ; [exact (proj2 c_encad) | exact (proj2 y_encad)].
+ assert (f_cont_interv : forall c : R, x <= c <= y -> continuity_pt f c).
+  intros c c_encad; apply derivable_continuous_pt ; apply pr. split.
+  apply Rlt_le_trans with (r2:=x) ; [exact (proj1 x_encad) | exact (proj1 c_encad)].
+  apply Rle_lt_trans with (r2:=y) ; [ exact (proj2 c_encad) | exact (proj2 y_encad)].
+ assert (id_cont_interv : forall c : R, x <= c <= y -> continuity_pt id c).
+  intros ; apply derivable_continuous_pt ; apply derivable_pt_id. 
+ elim (MVT f id x y derivable_f_interv derivable_id_interv x_lt_y f_cont_interv id_cont_interv).
+  intros c Temp ; elim Temp ; clear Temp ; intros Pr eq.
+   replace (id y - id x) with (y - x) in eq by intuition.
+   replace (derive_pt id c (derivable_id_interv c Pr)) with 1 in eq.
+   assert (Hyp : f y - f x > 0).
+    rewrite Rmult_1_r in eq. rewrite <- eq.
+    apply Rmult_gt_0_compat.
+    apply Rgt_minus ; assumption.
+    assert (c_encad2 : a <= c < b).
+     split.
+     apply Rlt_le ; apply Rlt_trans with (r2:=x) ; [exact (proj1 x_encad) | exact (proj1 Pr)].
+     apply Rle_lt_trans with (r2:=y) ; [apply Rlt_le ; exact (proj2 Pr) | exact (proj2 y_encad)].
+     assert (c_encad : a < c < b).
+      split.
+      apply Rlt_trans with (r2:=x) ; [exact (proj1 x_encad) | exact (proj1 Pr)].
+      apply Rle_lt_trans with (r2:=y) ; [apply Rlt_le ; exact (proj2 Pr) | exact (proj2 y_encad)].
+     assert (Temp := Df_gt_0 c c_encad).
+     assert (Temp2 := pr_nu f c (derivable_f_interv c Pr) (pr c c_encad)).
+     rewrite Temp2 ; apply Temp.
+   apply Rminus_gt ; exact Hyp.
+   symmetry ; rewrite derive_pt_eq ; apply derivable_pt_lim_id.
+Qed.
+
+(* begin hide *)
+Lemma plus_Rsqr_gt_0 : forall x, 1 + x ^ 2 > 0.
+Proof.
+intro m. replace 0 with (0+0) by intuition.
+ apply Rplus_gt_ge_compat. intuition.
+ elim (total_order_T m 0) ; intro s'. case s'.
+ intros m_cond. replace 0 with (0*0) by intuition.
+  replace (m ^ 2) with ((-m)^2).
+  apply Rle_ge ; apply Rmult_le_compat ; intuition ; apply Rlt_le ; rewrite Rmult_1_r ; intuition.
+  field.
+  intro H' ; rewrite H' ; right ; field.
+   left. intuition.
+Qed.
+(* end hide *)
+
+(* The following lemmas about PI should probably be in Rtrigo. *)
+
+Lemma PI2_lower_bound :
+  forall x, 0 < x < 2 -> 0 < cos x  -> x < PI/2.
+Proof.
+intros x [xp xlt2] cx.
+destruct (Rtotal_order x (PI/2)) as [xltpi2 | [xeqpi2 | xgtpi2]].
+  assumption.
+ now case (Rgt_not_eq _ _ cx); rewrite xeqpi2, cos_PI2.
+destruct (MVT_cor1 cos (PI/2) x derivable_cos xgtpi2) as
+   [c [Pc [cint1 cint2]]].
+revert Pc; rewrite cos_PI2, Rminus_0_r. 
+rewrite <- (pr_nu cos c (derivable_pt_cos c)), derive_pt_cos.
+assert (0 < c < 2) by (split; assert (t := PI2_RGT_0); fourier).
+assert (0 < sin c) by now apply sin_pos_tech.
+intros Pc.
+case (Rlt_not_le _ _ cx).
+rewrite <- (Rplus_0_l (cos x)), Pc, Ropp_mult_distr_l_reverse.
+apply Rle_minus, Rmult_le_pos;[apply Rlt_le; assumption | fourier ].
+Qed.
+
+Lemma PI2_3_2 : 3/2 < PI/2.
+Proof.
+apply PI2_lower_bound;[split; fourier | ].
+destruct (pre_cos_bound (3/2) 1) as [t _]; [fourier | fourier | ].
+apply Rlt_le_trans with (2 := t); clear t.
+unfold cos_approx; simpl; unfold cos_term.
+simpl mult; replace ((-1)^ 0) with 1 by ring; replace ((-1)^2) with 1 by ring;
+ replace ((-1)^4) with 1 by ring; replace ((-1)^1) with (-1) by ring;
+ replace ((-1)^3) with (-1) by ring; replace 3 with (IZR 3) by (simpl; ring);
+ replace 2 with (IZR 2) by (simpl; ring); simpl Z_of_nat;
+ rewrite !INR_IZR_INZ, Ropp_mult_distr_l_reverse, Rmult_1_l.
+match goal with |- _ < ?a =>
+replace a with ((- IZR 3 ^ 6 * IZR (Z_of_nat (fact 0)) * IZR (Z_of_nat (fact 2)) *
+    IZR (Z_of_nat (fact 4)) +
+    IZR 3 ^ 4 * IZR 2 ^ 2 * IZR (Z_of_nat (fact 0)) * IZR (Z_of_nat (fact 2)) *
+    IZR (Z_of_nat (fact 6)) -
+    IZR 3 ^ 2 * IZR 2 ^ 4 * IZR (Z_of_nat (fact 0)) * IZR (Z_of_nat (fact 4)) *
+    IZR (Z_of_nat (fact 6)) +
+    IZR 2 ^ 6 * IZR (Z_of_nat (fact 2)) * IZR (Z_of_nat (fact 4)) *
+    IZR (Z_of_nat (fact 6))) /
+   (IZR 2 ^ 6 * IZR (Z_of_nat (fact 0)) * IZR (Z_of_nat (fact 2)) *
+    IZR (Z_of_nat (fact 4)) * IZR (Z_of_nat (fact 6))));[ | field;
+    repeat apply conj;((rewrite <- INR_IZR_INZ; apply INR_fact_neq_0) ||
+         (apply Rgt_not_eq; apply (IZR_lt 0); reflexivity)) ]
+end.
+rewrite !fact_simpl, !inj_mult; simpl Z_of_nat.
+unfold Rdiv; apply Rmult_lt_0_compat.
+unfold Rminus; rewrite !pow_IZR, <- !opp_IZR, <- !mult_IZR, <- !opp_IZR, 
+  <- !plus_IZR; apply (IZR_lt 0); reflexivity.
+apply Rinv_0_lt_compat; rewrite !pow_IZR, <- !mult_IZR; apply (IZR_lt 0).
+reflexivity.
+Qed.
+
+Lemma PI2_1 : 1 < PI/2.
+Proof. assert (t := PI2_3_2); fourier. Qed.
+
+Lemma tan_increasing :
+  forall x y:R,
+    -PI/2 < x ->
+    x < y -> 
+    y < PI/2 -> tan x < tan y.
+Proof.
+intros x y Z_le_x x_lt_y y_le_1.
+ assert (x_encad : -PI/2 < x < PI/2).
+  split ; [assumption | apply Rlt_trans with (r2:=y) ; assumption].
+ assert (y_encad : -PI/2 < y < PI/2).
+  split ; [apply Rlt_trans with (r2:=x) ; intuition | intuition ].
+ assert (local_derivable_pt_tan : forall x : R, -PI/2 < x < PI/2 ->
+          derivable_pt tan x).
+  intros ; apply derivable_pt_tan ; intuition.
+ apply derive_increasing_interv with (a:=-PI/2) (b:=PI/2) (pr:=local_derivable_pt_tan) ; intuition.
+ fourier.
+ assert (Temp := pr_nu tan t (derivable_pt_tan t t_encad) (local_derivable_pt_tan t t_encad)) ;
+ rewrite <- Temp ; clear Temp.
+ assert (Temp := derive_pt_tan t t_encad) ; rewrite Temp ; clear Temp.
+ apply plus_Rsqr_gt_0.
+Qed.
+
+Lemma tan_is_inj : forall x y, -PI/2 < x < PI/2 -> -PI/2 < y < PI/2 ->
+   tan x = tan y -> x = y.
+Proof.
+  intros a b a_encad b_encad fa_eq_fb.
+  case(total_order_T a b).
+  intro s ; case s ; clear s.
+  intro Hf.
+  assert (Hfalse := tan_increasing a b (proj1 a_encad) Hf (proj2 b_encad)).
+  case (Rlt_not_eq (tan a) (tan b)) ; assumption.
+  intuition.
+  intro Hf. assert (Hfalse := tan_increasing b a (proj1 b_encad) Hf (proj2 a_encad)).
+  case (Rlt_not_eq (tan b) (tan a)) ; [|symmetry] ; assumption.
+Qed.
+
+Lemma exists_atan_in_frame :
+ forall lb ub y, lb < ub -> -PI/2 < lb -> ub < PI/2 ->
+ tan lb < y < tan ub -> {x | lb < x < ub /\ tan x = y}.
+Proof.
+intros lb ub y lb_lt_ub lb_cond ub_cond y_encad.
+ case y_encad ; intros y_encad1 y_encad2.
+     assert (f_cont : forall a : R, lb <= a <= ub -> continuity_pt tan a).
+      intros a a_encad. apply derivable_continuous_pt ; apply derivable_pt_tan.
+      split. apply Rlt_le_trans with (r2:=lb) ; intuition.
+      apply Rle_lt_trans with (r2:=ub) ; intuition.
+     assert (Cont : forall a : R, lb <= a <= ub -> continuity_pt (fun x => tan x - y) a).
+      intros a a_encad. unfold continuity_pt, continue_in, limit1_in, limit_in ; simpl ; unfold R_dist.
+      intros eps eps_pos. elim (f_cont a a_encad eps eps_pos).
+      intros alpha alpha_pos. destruct alpha_pos as (alpha_pos,Temp).
+      exists alpha. split.
+      assumption. intros x  x_cond.
+      replace (tan x - y - (tan a - y)) with (tan x - tan a) by field.
+      exact (Temp x x_cond).
+     assert (H1 : (fun x : R => tan x - y) lb < 0).
+       apply Rlt_minus. assumption.
+      assert (H2 : 0 < (fun x : R => tan x - y) ub).
+       apply Rgt_minus. assumption.
+     destruct (IVT_interv (fun x => tan x - y) lb ub Cont lb_lt_ub H1 H2) as (x,Hx).
+     exists x.
+     destruct Hx as (Hyp,Result).
+     intuition.
+     assert (Temp2 : x <> lb).
+      intro Hfalse. rewrite Hfalse in Result.
+      assert (Temp2 : y <> tan lb).
+       apply Rgt_not_eq ; assumption.
+      clear - Temp2 Result. apply Temp2.
+      intuition.
+     clear -Temp2 H3.
+      case H3 ; intuition. apply False_ind ; apply Temp2 ; symmetry ; assumption.
+      assert (Temp : x <> ub).
+      intro Hfalse. rewrite Hfalse in Result.
+      assert (Temp2 : y <> tan ub).
+       apply Rlt_not_eq ; assumption.
+      clear - Temp2 Result. apply Temp2.
+      intuition.
+      case H4 ; intuition.
+Qed.
+
+(** * Definition of arctangent as the reciprocal function of tangent and proof of this status *)
+Lemma tan_1_gt_1 : tan 1 > 1.
+Proof.
+assert (0 < cos 1) by (apply cos_gt_0; assert (t:=PI2_1); fourier).
+assert (t1 : cos 1 <= 1 - 1/2 + 1/24).
+ destruct (pre_cos_bound 1 0) as [_ t]; try fourier; revert t.
+ unfold cos_approx, cos_term; simpl; intros t; apply Rle_trans with (1:=t).
+ clear t; apply Req_le; field.
+assert (t2 : 1 - 1/6 <= sin 1).
+ destruct (pre_sin_bound 1 0) as [t _]; try fourier; revert t.
+ unfold sin_approx, sin_term; simpl; intros t; apply Rle_trans with (2:=t).
+ clear t; apply Req_le; field.
+pattern 1 at 2; replace 1 with
+  (cos 1 / cos 1) by (field; apply Rgt_not_eq; fourier).
+apply Rlt_gt; apply (Rmult_lt_compat_r (/ cos 1) (cos 1) (sin 1)).
+ apply Rinv_0_lt_compat; assumption.
+apply Rle_lt_trans with (1 := t1); apply Rlt_le_trans with (2 := t2).
+fourier.
+Qed.
+
+Definition frame_tan y : {x | 0 < x < PI/2 /\ Rabs y < tan x}.
+destruct (total_order_T (Rabs y) 1).
+ assert (yle1 : Rabs y <= 1) by (destruct s; fourier).
+ clear s; exists 1; split;[split; [exact Rlt_0_1 | exact PI2_1] | ].
+ apply Rle_lt_trans with (1 := yle1); exact tan_1_gt_1.
+assert (0 < / (Rabs y + 1)).
+ apply Rinv_0_lt_compat; fourier.
+set (u := /2 * / (Rabs y + 1)).
+assert (0 < u).
+ apply Rmult_lt_0_compat; [fourier | assumption].
+assert (vlt1 : / (Rabs y + 1) < 1).
+ apply Rmult_lt_reg_r with (Rabs y + 1).
+  assert (t := Rabs_pos y); fourier.
+ rewrite Rinv_l; [rewrite Rmult_1_l | apply Rgt_not_eq]; fourier.
+assert (vlt2 : u < 1).
+ apply Rlt_trans with (/ (Rabs y + 1)).
+  rewrite double_var.
+  assert (t : forall x, 0 < x -> x < x + x) by (clear; intros; fourier).
+  unfold u; rewrite Rmult_comm; apply t.
+  unfold Rdiv; rewrite Rmult_comm; assumption.
+ assumption.
+assert(int : 0 < PI / 2 - u < PI / 2).
+ split.
+  assert (t := PI2_1); apply Rlt_Rminus, Rlt_trans with (2 := t); assumption.
+ assert (dumb : forall x y, 0 < y -> x - y < x) by (clear; intros; fourier).
+ apply dumb; clear dumb; assumption.
+exists (PI/2 - u).
+assert (tmp : forall x y, 0 < x -> y < 1 -> x * y < x).
+ clear; intros x y x0 y1; pattern x at 2; rewrite <- (Rmult_1_r x).
+ apply Rmult_lt_compat_l; assumption.
+assert (0 < sin u).
+ apply sin_gt_0;[ assumption | ].
+ assert (t := PI2_Rlt_PI); assert (t' := PI2_1).
+ apply Rlt_trans with (2 := Rlt_trans _ _ _ t' t); assumption.
+split.
+ assumption.
+ apply Rlt_trans with (/2 * / cos(PI / 2 - u)).
+ rewrite cos_shift.
+ assert (sin u < u).
+  assert (t1 : 0 <= u) by (apply Rlt_le; assumption).
+  assert (t2 : u <= 4) by
+   (apply Rle_trans with 1;[apply Rlt_le | fourier]; assumption).
+  destruct (pre_sin_bound u 0 t1 t2) as [_ t].
+  apply Rle_lt_trans with (1 := t); clear t1 t2 t.
+  unfold sin_approx; simpl; unfold sin_term; simpl ((-1) ^ 0);
+  replace ((-1) ^ 2) with 1 by ring; simpl ((-1) ^ 1);
+  rewrite !Rmult_1_r, !Rmult_1_l; simpl plus; simpl (INR (fact 1)).
+  rewrite <- (fun x => tech_pow_Rmult x 0), <- (fun x => tech_pow_Rmult x 2),
+    <- (fun x => tech_pow_Rmult x 4).
+  rewrite (Rmult_comm (-1)); simpl ((/(Rabs y + 1)) ^ 0).
+  unfold Rdiv; rewrite Rinv_1, !Rmult_assoc, <- !Rmult_plus_distr_l.
+  apply tmp;[assumption | ].
+  rewrite Rplus_assoc, Rmult_1_l; pattern 1 at 3; rewrite <- Rplus_0_r.
+  apply Rplus_lt_compat_l.
+  rewrite <- Rmult_assoc.
+  match goal with |- (?a * (-1)) + _ < 0 =>
+   rewrite <- (Rplus_opp_l a), Ropp_mult_distr_r_reverse, Rmult_1_r
+  end.
+  apply Rplus_lt_compat_l.
+  assert (0 < u ^ 2) by (apply pow_lt; assumption).
+  replace (u ^ 4) with (u ^ 2 * u ^ 2) by ring.
+ rewrite Rmult_assoc; apply Rmult_lt_compat_l; auto.
+  apply Rlt_trans with (u ^ 2 * /INR (fact 3)).
+   apply Rmult_lt_compat_l; auto.
+   apply Rinv_lt_contravar.
+    solve[apply Rmult_lt_0_compat; apply INR_fact_lt_0].
+   rewrite !INR_IZR_INZ; apply IZR_lt; reflexivity.
+  rewrite Rmult_comm; apply tmp.
+   solve[apply Rinv_0_lt_compat, INR_fact_lt_0].
+  apply Rlt_trans with (2 := vlt2).
+  simpl; unfold u; apply tmp; auto; rewrite Rmult_1_r; assumption.
+ apply Rlt_trans with (Rabs y + 1);[fourier | ]. 
+ pattern (Rabs y + 1) at 1; rewrite <- (Rinv_involutive (Rabs y + 1));
+  [ | apply Rgt_not_eq; fourier].
+ rewrite <- Rinv_mult_distr.
+   apply Rinv_lt_contravar.
+    apply Rmult_lt_0_compat.
+     apply Rmult_lt_0_compat;[fourier | assumption].
+    assumption.
+   replace (/(Rabs y + 1)) with (2 * u).
+    fourier.
+   unfold u; field; apply Rgt_not_eq; clear -r; fourier.
+  solve[discrR].
+ apply Rgt_not_eq; assumption.
+unfold tan.
+set (u' := PI / 2); unfold Rdiv; apply Rmult_lt_compat_r; unfold u'.
+ apply Rinv_0_lt_compat. 
+ rewrite cos_shift; assumption.
+assert (vlt3 : u < /4).
+ replace (/4) with (/2 * /2) by field.
+ unfold u; apply Rmult_lt_compat_l;[fourier | ].
+ apply Rinv_lt_contravar.
+  apply Rmult_lt_0_compat; fourier.
+ fourier.
+assert (1 < PI / 2 - u) by (assert (t := PI2_3_2); fourier).
+apply Rlt_trans with (sin 1).
+ assert (t' : 1 <= 4) by fourier.
+ destruct (pre_sin_bound 1 0 (Rlt_le _ _ Rlt_0_1) t') as [t _].
+ apply Rlt_le_trans with (2 := t); clear t.
+ simpl plus; replace (sin_approx 1 1) with (5/6);[fourier | ].
+ unfold sin_approx, sin_term; simpl; field.
+apply sin_increasing_1.
+    assert (t := PI2_1); fourier.
+   apply Rlt_le, PI2_1.
+  assert (t := PI2_1); fourier.
+ fourier.
+assumption.
+Qed.
+
+Lemma ub_opp : forall x, x < PI/2 -> -PI/2 < -x.
+Proof.
+intros x h; rewrite Ropp_div; apply Ropp_lt_contravar; assumption.
+Qed.
+
+Lemma pos_opp_lt : forall x, 0 < x -> -x < x.
+Proof. intros; fourier. Qed.
+
+Lemma tech_opp_tan : forall x y, -tan x < y -> tan (-x) < y.
+intros; rewrite tan_neg; assumption.
+Qed.
+
+Definition pre_atan (y : R) : {x : R | -PI/2 < x < PI/2 /\ tan x = y}.
+destruct (frame_tan y) as [ub [[ub0 ubpi2] Ptan_ub]].
+set (pr := (conj (tech_opp_tan _ _ (proj2 (Rabs_def2 _ _ Ptan_ub)))
+     (proj1 (Rabs_def2 _ _ Ptan_ub)))).
+destruct (exists_atan_in_frame (-ub) ub y (pos_opp_lt _ ub0) (ub_opp _ ubpi2)
+             ubpi2 pr) as [v [[vl vu] vq]].
+exists v; clear pr.
+split;[rewrite Ropp_div; split; fourier | assumption].
+Qed.
+
+Definition atan x := let (v, _) := pre_atan x in v.
+
+Lemma atan_bound : forall x, -PI/2 < atan x < PI/2.
+Proof.
+intros x; unfold atan; destruct (pre_atan x) as [v [int _]]; exact int.
+Qed.
+
+Lemma atan_right_inv : forall x, tan (atan x) = x.
+Proof.
+intros x; unfold atan; destruct (pre_atan x) as [v [_ q]]; exact q.
+Qed.
+
+Lemma atan_opp : forall x, atan (- x) = - atan x.
+Proof.
+intros x; generalize (atan_bound (-x)); rewrite Ropp_div;intros [a b].
+generalize (atan_bound x); rewrite Ropp_div; intros [c d].
+apply tan_is_inj; try rewrite Ropp_div; try split; try fourier.
+rewrite tan_neg, !atan_right_inv; reflexivity.
+Qed.
+
+Lemma derivable_pt_atan : forall x, derivable_pt atan x.
+Proof.
+intros x.
+destruct (frame_tan x) as [ub [[ub0 ubpi] P]].
+assert (lb_lt_ub : -ub < ub) by apply pos_opp_lt, ub0.
+assert (xint : tan(-ub) < x < tan ub).
+ assert (xint' : x < tan ub /\ -(tan ub) < x) by apply Rabs_def2, P.
+  rewrite tan_neg; tauto.
+assert (inv_p : forall x, tan(-ub) <= x -> x <= tan ub -> 
+                     comp tan atan x = id x).
+ intros; apply atan_right_inv.
+assert (int_tan : forall y, tan (- ub) <= y -> y <= tan ub ->
+                       -ub <= atan y <= ub).
+ clear -ub0 ubpi; intros y lo up; split.
+  destruct (Rle_lt_dec (-ub) (atan y)) as [h | abs]; auto.
+  assert (y < tan (-ub)).
+   rewrite <- (atan_right_inv y); apply tan_increasing.
+     destruct (atan_bound y); assumption.
+    assumption.
+   fourier.
+  fourier.
+ destruct (Rle_lt_dec (atan y) ub) as [h | abs]; auto.
+  assert (tan ub < y).
+   rewrite <- (atan_right_inv y); apply tan_increasing.
+    rewrite Ropp_div; fourier.
+   assumption.
+  destruct (atan_bound y); assumption.
+ fourier.
+assert (incr : forall x y, -ub <= x -> x < y -> y <= ub -> tan x < tan y).
+ intros y z l yz u; apply tan_increasing.
+   rewrite Ropp_div; fourier.
+  assumption.
+ fourier.
+assert (der : forall a, -ub <= a <= ub -> derivable_pt tan a).
+ intros a [la ua]; apply derivable_pt_tan.
+ rewrite Ropp_div; split; fourier.
+assert (df_neq : derive_pt tan (atan x)
+     (derivable_pt_recip_interv_prelim1 tan atan 
+        (- ub) ub x lb_lt_ub xint inv_p int_tan incr der) <> 0).
+ rewrite <- (pr_nu tan (atan x)
+              (derivable_pt_tan (atan x) (atan_bound x))).
+ rewrite derive_pt_tan.
+ solve[apply Rgt_not_eq, plus_Rsqr_gt_0].
+apply (derivable_pt_recip_interv tan atan (-ub) ub x
+      lb_lt_ub xint inv_p int_tan incr der).
+exact df_neq.
+Qed.
+
+Lemma atan_increasing : forall x y, x < y -> atan x < atan y.
+intros x y d.
+assert (t1 := atan_bound x).
+assert (t2 := atan_bound y).
+destruct (Rlt_le_dec (atan x) (atan y)) as [lt | bad].
+ assumption.
+apply Rlt_not_le in d.
+case d.
+rewrite <- (atan_right_inv y), <- (atan_right_inv x).
+destruct bad as [ylt | yx].
+ apply Rlt_le, tan_increasing; try tauto.
+solve[rewrite yx; apply Rle_refl].
+Qed.
+
+Lemma atan_0 : atan 0 = 0.
+apply tan_is_inj; try (apply atan_bound).
+ assert (t := PI_RGT_0); rewrite Ropp_div; split; fourier.
+rewrite atan_right_inv, tan_0.
+reflexivity.
+Qed.
+
+Lemma atan_1 : atan 1 = PI/4.
+assert (ut := PI_RGT_0).
+assert (-PI/2 < PI/4 < PI/2) by (rewrite Ropp_div; split; fourier).
+assert (t := atan_bound 1).
+apply tan_is_inj; auto.
+rewrite tan_PI4, atan_right_inv; reflexivity.
+Qed.
+
+(** atan's derivative value is the function 1 / (1+x²) *)
+
+Lemma derive_pt_atan : forall x,
+      derive_pt atan x (derivable_pt_atan x) =
+         1 / (1 + x²).
+Proof.
+intros x.
+destruct (frame_tan x) as [ub [[ub0 ubpi] Pub]].
+assert (lb_lt_ub : -ub < ub) by apply pos_opp_lt, ub0.
+assert (xint : tan(-ub) < x < tan ub).
+ assert (xint' : x < tan ub /\ -(tan ub) < x) by apply Rabs_def2, Pub.
+  rewrite tan_neg; tauto.
+assert (inv_p : forall x, tan(-ub) <= x -> x <= tan ub -> 
+                     comp tan atan x = id x).
+ intros; apply atan_right_inv.
+assert (int_tan : forall y, tan (- ub) <= y -> y <= tan ub ->
+                       -ub <= atan y <= ub).
+ clear -ub0 ubpi; intros y lo up; split.
+  destruct (Rle_lt_dec (-ub) (atan y)) as [h | abs]; auto.
+  assert (y < tan (-ub)).
+   rewrite <- (atan_right_inv y); apply tan_increasing.
+     destruct (atan_bound y); assumption.
+    assumption.
+   fourier.
+  fourier.
+ destruct (Rle_lt_dec (atan y) ub) as [h | abs]; auto.
+  assert (tan ub < y).
+   rewrite <- (atan_right_inv y); apply tan_increasing.
+    rewrite Ropp_div; fourier.
+   assumption.
+  destruct (atan_bound y); assumption.
+ fourier.
+assert (incr : forall x y, -ub <= x -> x < y -> y <= ub -> tan x < tan y).
+ intros y z l yz u; apply tan_increasing.
+   rewrite Ropp_div; fourier.
+  assumption.
+ fourier.
+assert (der : forall a, -ub <= a <= ub -> derivable_pt tan a).
+ intros a [la ua]; apply derivable_pt_tan.
+ rewrite Ropp_div; split; fourier.
+assert (df_neq : derive_pt tan (atan x)
+     (derivable_pt_recip_interv_prelim1 tan atan 
+        (- ub) ub x lb_lt_ub xint inv_p int_tan incr der) <> 0).
+ rewrite <- (pr_nu tan (atan x)
+              (derivable_pt_tan (atan x) (atan_bound x))).
+ rewrite derive_pt_tan.
+ solve[apply Rgt_not_eq, plus_Rsqr_gt_0].
+assert (t := derive_pt_recip_interv tan atan (-ub) ub x lb_lt_ub
+        xint incr int_tan der inv_p df_neq).
+rewrite <- (pr_nu atan x (derivable_pt_recip_interv tan atan (- ub) ub
+      x lb_lt_ub xint inv_p int_tan incr der df_neq)).
+rewrite t.
+assert (t' := atan_bound x).
+rewrite <- (pr_nu tan (atan x) (derivable_pt_tan _ t')). 
+rewrite derive_pt_tan, atan_right_inv.
+replace (Rsqr x) with (x ^ 2) by (unfold Rsqr; ring).
+reflexivity.
+Qed.
+
+(** * Definition of the arctangent function as the sum of the arctan power series *)
+(* Proof taken from Guillaume Melquiond's interval package for Coq *)
+
+Definition Ratan_seq x :=  fun n => (x ^ (2 * n + 1) / INR (2 * n + 1))%R.
+
+Lemma Ratan_seq_decreasing : forall x, (0 <= x <= 1)%R -> Un_decreasing (Ratan_seq x).
+Proof.
+intros x Hx n.
+ unfold Ratan_seq, Rdiv.
+ apply Rmult_le_compat. apply pow_le.
+ exact (proj1 Hx).
+ apply Rlt_le.
+ apply Rinv_0_lt_compat.
+ apply lt_INR_0.
+ omega.
+ destruct (proj1 Hx) as [Hx1|Hx1].
+ destruct (proj2 Hx) as [Hx2|Hx2].
+ (* . 0 < x < 1 *)
+ rewrite <- (Rinv_involutive x).
+ assert (/ x <> 0)%R by auto with real.
+ repeat rewrite <- Rinv_pow with (1 := H).
+ apply Rlt_le.
+ apply Rinv_lt_contravar.
+ apply Rmult_lt_0_compat ; apply pow_lt ; auto with real.
+ apply Rlt_pow.
+ rewrite <- Rinv_1.
+ apply Rinv_lt_contravar.
+ rewrite Rmult_1_r.
+ exact Hx1.
+ exact Hx2.
+ omega.
+ apply Rgt_not_eq.
+ exact Hx1.
+ (* . x = 1 *)
+ rewrite Hx2.
+ do 2 rewrite pow1.
+ apply Rle_refl.
+ (* . x = 0 *)
+ rewrite <- Hx1.
+ do 2 (rewrite pow_i ; [ idtac | omega ]).
+ apply Rle_refl.
+ apply Rlt_le.
+ apply Rinv_lt_contravar.
+ apply Rmult_lt_0_compat ; apply lt_INR_0 ; omega.
+ apply lt_INR.
+ omega.
+Qed.
+
+Lemma Ratan_seq_converging : forall x, (0 <= x <= 1)%R -> Un_cv (Ratan_seq x) 0.
+Proof.
+intros x Hx eps Heps.
+ destruct (archimed (/ eps)) as (HN,_).
+ assert (0 < up (/ eps))%Z.
+  apply lt_IZR.
+  apply Rlt_trans with (2 := HN).
+  apply Rinv_0_lt_compat.
+  exact Heps.
+ case_eq (up (/ eps)) ;
+  intros ; rewrite H0 in H ; try discriminate H.
+   rewrite H0 in HN.
+   simpl in HN.
+   pose (N := nat_of_P p).
+   fold N in HN.
+   clear H H0.
+   exists N.
+  intros n Hn.
+   unfold R_dist.
+   rewrite Rminus_0_r.
+   unfold Ratan_seq.
+   rewrite Rabs_right.
+   apply Rle_lt_trans with (1 ^ (2 * n + 1) / INR (2 * n + 1))%R.
+   unfold Rdiv.
+   apply Rmult_le_compat_r.
+   apply Rlt_le.
+   apply Rinv_0_lt_compat.
+   apply lt_INR_0.
+   omega.
+   apply pow_incr.
+   exact Hx.
+   rewrite pow1.
+   apply Rle_lt_trans with (/ INR (2 * N + 1))%R.
+   unfold Rdiv.
+   rewrite Rmult_1_l.
+   apply Rle_Rinv.
+   apply lt_INR_0.
+   omega.
+   replace 0 with (INR 0) by intuition.
+   apply lt_INR.
+   omega.
+   intuition.
+   rewrite <- (Rinv_involutive eps).
+   apply Rinv_lt_contravar.
+   apply Rmult_lt_0_compat.
+   auto with real.
+   apply lt_INR_0.
+   omega.
+   apply Rlt_trans with (INR N).
+   destruct (archimed (/ eps)) as (H,_).
+   assert (0 < up (/ eps))%Z.
+   apply lt_IZR.
+   apply Rlt_trans with (2 := H).
+   apply Rinv_0_lt_compat.
+   exact Heps.
+   exact HN.
+   apply lt_INR.
+   omega.
+   apply Rgt_not_eq.
+   exact Heps.
+   apply Rle_ge.
+   unfold Rdiv.
+   apply Rmult_le_pos.
+   apply pow_le.
+   exact (proj1 Hx).
+   apply Rlt_le.
+   apply Rinv_0_lt_compat.
+   apply lt_INR_0.
+   omega.
+Qed.
+
+Definition ps_atan_exists_01 (x : R) (Hx:0 <= x <= 1) :
+   {l : R | Un_cv (fun N : nat => sum_f_R0 (tg_alt (Ratan_seq x)) N) l}.
+exact (alternated_series (Ratan_seq x)
+  (Ratan_seq_decreasing _ Hx) (Ratan_seq_converging _ Hx)).
+Defined.
+
+Lemma Ratan_seq_opp : forall x n, Ratan_seq (-x) n = -Ratan_seq x n.
+Proof.
+intros x n; unfold Ratan_seq.
+rewrite !pow_add, !pow_mult, !pow_1.
+unfold Rdiv; replace ((-x) ^ 2) with (x ^ 2) by ring; ring.
+Qed.
+
+Lemma sum_Ratan_seq_opp : 
+  forall x n, sum_f_R0 (tg_alt (Ratan_seq (- x))) n =
+     - sum_f_R0 (tg_alt (Ratan_seq x)) n.
+Proof.
+intros x n; replace (-sum_f_R0 (tg_alt (Ratan_seq x)) n) with 
+  (-1 * sum_f_R0 (tg_alt (Ratan_seq x)) n) by ring.
+rewrite scal_sum; apply sum_eq; intros i _; unfold tg_alt.
+rewrite Ratan_seq_opp; ring.
+Qed.
+
+Definition ps_atan_exists_1 (x : R) (Hx : -1 <= x <= 1) :
+   {l : R | Un_cv (fun N : nat => sum_f_R0 (tg_alt (Ratan_seq x)) N) l}.
+destruct (Rle_lt_dec 0 x).
+ assert (pr : 0 <= x <= 1) by tauto.
+ exact (ps_atan_exists_01 x pr).
+assert (pr : 0 <= -x <= 1) by (destruct Hx; split; fourier).
+destruct (ps_atan_exists_01 _ pr) as [v Pv].
+exists (-v).
+ apply (Un_cv_ext (fun n => (- 1) * sum_f_R0 (tg_alt (Ratan_seq (- x))) n)).
+ intros n; rewrite sum_Ratan_seq_opp; ring.
+replace (-v) with (-1 * v) by ring.
+apply CV_mult;[ | assumption].
+solve[intros; exists 0%nat; intros; rewrite R_dist_eq; auto].
+Qed.
+
+Definition in_int (x : R) : {-1 <= x <= 1}+{~ -1 <= x <= 1}.
+destruct (Rle_lt_dec x 1).
+ destruct (Rle_lt_dec (-1) x).
+  left;split; auto.
+ right;intros [a1 a2]; fourier.
+right;intros [a1 a2]; fourier.
+Qed.
+
+Definition ps_atan (x : R) : R :=
+ match in_int x with
+   left h => let (v, _) := ps_atan_exists_1 x h in v
+ | right h => atan x
+ end.
+
+(** * Proof of the equivalence of the two definitions between -1 and 1 *)
+
+Lemma ps_atan0_0 : ps_atan 0 = 0.
+Proof.
+unfold ps_atan.
+ destruct (in_int 0) as [h1 | h2].
+ destruct (ps_atan_exists_1 0 h1) as [v P].
+ apply (UL_sequence _ _ _ P).
+  apply (Un_cv_ext (fun n => 0)).
+  symmetry;apply sum_eq_R0.
+  intros i _; unfold tg_alt, Ratan_seq; rewrite plus_comm; simpl.
+  unfold Rdiv; rewrite !Rmult_0_l, Rmult_0_r; reflexivity.
+ intros eps ep; exists 0%nat; intros n _; unfold R_dist.
+ rewrite Rminus_0_r, Rabs_pos_eq; auto with real.
+case h2; split; fourier.
+Qed.
+
+Lemma ps_atan_exists_1_opp :
+  forall x h h', proj1_sig (ps_atan_exists_1 (-x) h) = 
+     -(proj1_sig (ps_atan_exists_1 x h')).
+Proof.
+intros x h h'; destruct (ps_atan_exists_1 (-x) h) as [v Pv].
+destruct (ps_atan_exists_1 x h') as [u Pu]; simpl.
+assert (Pu' : Un_cv (fun N => (-1) * sum_f_R0 (tg_alt (Ratan_seq x)) N) (-1 * u)).
+ apply CV_mult;[ | assumption].
+ intros eps ep; exists 0%nat; intros; rewrite R_dist_eq; assumption.  
+assert (Pv' : Un_cv
+           (fun N : nat => -1 * sum_f_R0 (tg_alt (Ratan_seq x)) N) v).
+ apply Un_cv_ext with (2 := Pv); intros n; rewrite sum_Ratan_seq_opp; ring.
+replace (-u) with (-1 * u) by ring.
+apply UL_sequence with (1:=Pv') (2:= Pu').
+Qed.
+
+Lemma ps_atan_opp : forall x, ps_atan (-x) = -ps_atan x.
+Proof.
+intros x; unfold ps_atan.
+destruct (in_int (- x)) as [inside | outside].
+ destruct (in_int x) as [ins' | outs'].
+ generalize (ps_atan_exists_1_opp x inside ins').
+  intros h; exact h.
+ destruct inside; case outs'; split; fourier.   
+destruct (in_int x) as [ins' | outs'].
+ destruct outside; case ins'; split; fourier.   
+apply atan_opp.
+Qed.
+
+(** atan = ps_atan *)
+
+Lemma ps_atanSeq_continuity_pt_1 : forall (N:nat) (x:R),
+      0 <= x ->
+      x <= 1 ->
+      continuity_pt (fun x => sum_f_R0 (tg_alt (Ratan_seq x)) N) x.
+Proof.
+assert (Sublemma : forall (x:R) (N:nat), sum_f_R0 (tg_alt (Ratan_seq x)) N = x * (comp (fun x => sum_f_R0 (fun n => (fun i : nat => (-1) ^ i / INR (2 * i + 1)) n * x ^ n) N) (fun x => x ^ 2) x)).
+ intros x N.
+  induction N.
+   unfold tg_alt, Ratan_seq, comp ; simpl ; field.
+   simpl sum_f_R0 at 1.
+   rewrite IHN.
+   replace (comp (fun x => sum_f_R0 (fun n : nat => (-1) ^ n / INR (2 * n + 1) * x ^ n) (S N)) (fun x => x ^ 2))
+     with (comp (fun x => sum_f_R0 (fun n : nat => (-1) ^ n / INR (2 * n + 1) * x ^ n) N + (-1) ^ (S N) / INR (2 * (S N) + 1) * x ^ (S N)) (fun x => x ^ 2)).
+   unfold comp.
+   rewrite Rmult_plus_distr_l.
+   apply Rplus_eq_compat_l.
+   unfold tg_alt, Ratan_seq.
+   rewrite <- Rmult_assoc.
+   case (Req_dec x 0) ; intro Hyp.
+   rewrite Hyp ; rewrite pow_i. rewrite Rmult_0_l ; rewrite Rmult_0_l.
+   unfold Rdiv ; rewrite Rmult_0_l ; rewrite Rmult_0_r ; reflexivity.
+   intuition.
+   replace (x * ((-1) ^ S N / INR (2 * S N + 1)) * (x ^ 2) ^ S N) with (x ^ (2 * S N + 1) * ((-1) ^ S N / INR (2 * S N + 1))).
+   rewrite Rmult_comm ; unfold Rdiv at 1.
+   rewrite Rmult_assoc ; apply Rmult_eq_compat_l.
+   field. apply Rgt_not_eq ; intuition.
+   rewrite Rmult_assoc.
+   replace (x * ((-1) ^ S N / INR (2 * S N + 1) * (x ^ 2) ^ S N)) with (((-1) ^ S N / INR (2 * S N + 1) * (x ^ 2) ^ S N) * x).
+   rewrite Rmult_assoc.
+   replace ((x ^ 2) ^ S N * x) with (x ^ (2 * S N + 1)).
+   rewrite Rmult_comm at 1 ; reflexivity.
+   rewrite <- pow_mult.
+   assert (Temp : forall x n, x ^ n * x = x ^ (n+1)).
+    intros a n ; induction n. rewrite pow_O. simpl ; intuition.
+    simpl ; rewrite Rmult_assoc ; rewrite IHn ; intuition.
+   rewrite Temp ; reflexivity.
+   rewrite Rmult_comm ; reflexivity.
+   intuition.
+intros N x x_lb x_ub.
+ intros eps eps_pos.
+ assert (continuity_id : continuity id).
+ apply derivable_continuous ; exact derivable_id.
+assert (Temp := continuity_mult id (comp
+        (fun x1 : R =>
+         sum_f_R0 (fun n : nat => (-1) ^ n / INR (2 * n + 1) * x1 ^ n) N)
+        (fun x1 : R => x1 ^ 2))
+           continuity_id).
+assert (Temp2 : continuity
+    (comp
+       (fun x1 : R =>
+        sum_f_R0 (fun n : nat => (-1) ^ n / INR (2 * n + 1) * x1 ^ n) N)
+       (fun x1 : R => x1 ^ 2))).
+ apply continuity_comp.
+ reg.
+ apply continuity_finite_sum.
+ elim (Temp Temp2 x eps eps_pos) ; clear Temp Temp2 ; intros alpha T ; destruct T as (alpha_pos, T).
+ exists alpha ; split.
+ intuition.
+intros x0 x0_cond.
+ rewrite Sublemma ; rewrite Sublemma.
+apply T.
+intuition.
+Qed.
+
+(** Definition of ps_atan's derivative *)
+
+Definition Datan_seq := fun (x:R) (n:nat) => x ^ (2*n).
+
+Lemma pow_lt_1_compat : forall x n, 0 <= x < 1 -> (0 < n)%nat ->
+   0 <= x ^ n < 1.
+Proof.
+intros x n hx; induction 1; simpl.
+ rewrite Rmult_1_r; tauto.
+split.
+ apply Rmult_le_pos; tauto.
+rewrite <- (Rmult_1_r 1); apply Rmult_le_0_lt_compat; intuition.
+Qed.
+
+Lemma Datan_seq_Rabs : forall x n, Datan_seq (Rabs x) n = Datan_seq x n.
+Proof.
+intros x n; unfold Datan_seq; rewrite !pow_mult, pow2_abs; reflexivity.
+Qed.
+
+Lemma Datan_seq_pos : forall x n, 0 < x -> 0 < Datan_seq x n.
+Proof.
+intros x n x_lb ; unfold Datan_seq ; induction n.
+ simpl ; intuition.
+ replace (x ^ (2 * S n)) with ((x ^ 2) * (x ^ (2 * n))).
+ apply Rmult_gt_0_compat.
+ replace (x^2) with (x*x) by field ; apply Rmult_gt_0_compat ; assumption.
+ assumption.
+ replace (2 * S n)%nat with (S (S (2 * n))) by intuition.
+ simpl ; field.
+Qed.
+
+Lemma Datan_sum_eq :forall x n,
+  sum_f_R0 (tg_alt (Datan_seq x)) n = (1 - (- x ^ 2) ^ S n)/(1 + x ^ 2).
+Proof.
+intros x n.
+assert (dif : - x ^ 2 <> 1).
+apply Rlt_not_eq; apply Rle_lt_trans with 0;[ | apply Rlt_0_1].
+assert (t := pow2_ge_0 x); fourier.
+replace (1 + x ^ 2) with (1 - - (x ^ 2)) by ring; rewrite <- (tech3 _ n dif).
+apply sum_eq; unfold tg_alt, Datan_seq; intros i _.
+rewrite pow_mult, <- Rpow_mult_distr, Ropp_mult_distr_l_reverse, Rmult_1_l.
+reflexivity.
+Qed.
+
+Lemma Datan_seq_increasing : forall x y n, (n > 0)%nat -> 0 <= x < y -> Datan_seq x n < Datan_seq y n.
+Proof.
+intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition.
+ assert (y_pos : y > 0). apply Rle_lt_trans with (r2:=x) ; intuition.
+ induction n.
+ apply False_ind ; intuition.
+ clear -x_encad x_pos y_pos ; induction n ; unfold Datan_seq.
+ case x_pos ; clear x_pos ; intro x_pos.
+ simpl ; apply Rmult_gt_0_lt_compat ; intuition. fourier.
+ rewrite x_pos ; rewrite pow_i. replace (y ^ (2*1)) with (y*y).
+ apply Rmult_gt_0_compat ; assumption.
+ simpl ; field.
+ intuition.
+ assert (Hrew : forall a, a^(2 * S (S n)) = (a ^ 2) * (a ^ (2 * S n))).
+  clear ; intro a ; replace (2 * S (S n))%nat with (S (S (2 * S n)))%nat by intuition.
+  simpl ; field.
+ case x_pos ; clear x_pos ; intro x_pos.
+ rewrite Hrew ; rewrite Hrew.
+ apply Rmult_gt_0_lt_compat ; intuition.
+ apply Rmult_gt_0_lt_compat ; intuition ; fourier.
+ rewrite x_pos.
+ rewrite pow_i ; intuition.
+Qed.
+
+Lemma Datan_seq_decreasing : forall x,  -1 < x -> x < 1 -> Un_decreasing (Datan_seq x).
+Proof.
+intros x x_lb x_ub n.
+unfold Datan_seq.
+replace (2 * S n)%nat with (2 + 2 * n)%nat by ring.
+rewrite <- (Rmult_1_l (x ^ (2 * n))).
+rewrite pow_add.
+apply Rmult_le_compat_r.
+rewrite pow_mult; apply pow_le, pow2_ge_0.
+apply Rlt_le; rewrite <- pow2_abs.
+assert (intabs : 0 <= Rabs x < 1).
+ split;[apply Rabs_pos | apply Rabs_def1]; tauto.
+apply (pow_lt_1_compat (Rabs x) 2) in intabs.
+ tauto.
+omega.
+Qed.
+
+Lemma Datan_seq_CV_0 : forall x, -1 < x -> x < 1 -> Un_cv (Datan_seq x) 0.
+Proof.
+intros x x_lb x_ub eps eps_pos.
+assert (x_ub2 : Rabs (x^2) < 1).
+ rewrite Rabs_pos_eq;[ | apply pow2_ge_0].
+ rewrite <- pow2_abs.
+ assert (H: 0 <= Rabs x < 1)
+   by (split;[apply Rabs_pos | apply Rabs_def1; auto]).
+ apply (pow_lt_1_compat _ 2) in H;[tauto | omega].
+elim (pow_lt_1_zero (x^2) x_ub2 eps eps_pos) ; intros N HN ; exists N ; intros n Hn.
+unfold R_dist, Datan_seq.
+replace (x ^ (2 * n) - 0) with ((x ^ 2) ^ n). apply HN ; assumption.
+rewrite pow_mult ; field.
+Qed.
+
+Lemma Datan_lim : forall x, -1 < x -> x < 1 ->
+    Un_cv (fun N : nat => sum_f_R0 (tg_alt (Datan_seq x)) N) (/ (1 + x ^ 2)).
+Proof.
+intros x x_lb x_ub eps eps_pos.
+assert (Tool0 : 0 <= x ^ 2) by apply pow2_ge_0.
+assert (Tool1 : 0 < (1 + x ^ 2)).
+ solve[apply Rplus_lt_le_0_compat ; intuition].
+assert (Tool2 : / (1 + x ^ 2) > 0).
+ apply Rinv_0_lt_compat ; tauto.
+assert (x_ub2' : 0<= Rabs (x^2) < 1).
+ rewrite Rabs_pos_eq, <- pow2_abs;[ | apply pow2_ge_0].
+ apply pow_lt_1_compat;[split;[apply Rabs_pos | ] | omega].
+ apply Rabs_def1; assumption.
+assert (x_ub2 : Rabs (x^2) < 1) by tauto.
+assert (eps'_pos : ((1+x^2)*eps) > 0).
+  apply Rmult_gt_0_compat ; assumption.
+elim (pow_lt_1_zero _ x_ub2 _ eps'_pos) ; intros N HN ; exists N.
+intros n Hn.
+assert (H1 : - x^2 <> 1).
+ apply Rlt_not_eq; apply Rle_lt_trans with (2 := Rlt_0_1).
+assert (t := pow2_ge_0 x); fourier.
+rewrite Datan_sum_eq. 
+unfold R_dist.
+assert (tool : forall a b, a / b - /b = (-1 + a) /b).
+ intros a b; rewrite <- (Rmult_1_l (/b)); unfold Rdiv, Rminus.
+ rewrite <- Ropp_mult_distr_l_reverse, Rmult_plus_distr_r, Rplus_comm.
+ reflexivity.
+set (u := 1 + x ^ 2); rewrite tool; unfold Rminus; rewrite <- Rplus_assoc.
+unfold Rdiv, u.
+rewrite Rplus_opp_l, Rplus_0_l, Ropp_mult_distr_l_reverse, Rabs_Ropp.
+rewrite Rabs_mult; clear tool u.
+assert (tool : forall k, Rabs ((-x ^ 2) ^ k) = Rabs ((x ^ 2) ^ k)).
+ clear -Tool0; induction k;[simpl; rewrite Rabs_R1;tauto | ].
+ rewrite <- !(tech_pow_Rmult _ k), !Rabs_mult, Rabs_Ropp, IHk, Rabs_pos_eq.
+  reflexivity.
+ exact Tool0.
+rewrite tool, (Rabs_pos_eq (/ _)); clear tool;[ | apply Rlt_le; assumption].
+assert (tool : forall a b c, 0 < b -> a < b * c -> a * / b < c).
+ intros a b c bp h; replace c with (b * c * /b).
+  apply Rmult_lt_compat_r.  
+   apply Rinv_0_lt_compat; assumption.
+  assumption.
+ field; apply Rgt_not_eq; exact bp.
+apply tool;[exact Tool1 | ].
+apply HN; omega.
+Qed.
+
+Lemma Datan_CVU_prelim : forall c (r : posreal), Rabs c + r < 1 ->
+ CVU (fun N x => sum_f_R0 (tg_alt (Datan_seq x)) N)
+     (fun y : R => / (1 + y ^ 2)) c r.
+Proof.
+intros c r ub_ub eps eps_pos.
+apply (Alt_CVU (fun x n => Datan_seq n x) 
+         (fun x => /(1 + x ^ 2))
+         (Datan_seq (Rabs c + r)) c r).
+     intros x inb; apply Datan_seq_decreasing;
+      try (apply Boule_lt in inb; apply Rabs_def2 in inb;
+         destruct inb; fourier).
+    intros x inb; apply Datan_seq_CV_0;
+      try (apply Boule_lt in inb; apply Rabs_def2 in inb;
+         destruct inb; fourier).
+   intros x inb; apply (Datan_lim x);
+      try (apply Boule_lt in inb; apply Rabs_def2 in inb;
+         destruct inb; fourier).
+  intros x [ | n] inb.
+   solve[unfold Datan_seq; apply Rle_refl].
+  rewrite <- (Datan_seq_Rabs x); apply Rlt_le, Datan_seq_increasing.
+   omega.
+  apply Boule_lt in inb; intuition.
+  solve[apply Rabs_pos].
+ apply Datan_seq_CV_0.
+  apply Rlt_trans with 0;[fourier | ].
+  apply Rplus_le_lt_0_compat.
+   solve[apply Rabs_pos].
+  destruct r; assumption.
+ assumption.
+assumption.
+Qed.
+
+Lemma Datan_is_datan : forall (N:nat) (x:R),
+      -1 <= x ->
+      x < 1 ->
+derivable_pt_lim (fun x => sum_f_R0 (tg_alt (Ratan_seq x)) N) x (sum_f_R0 (tg_alt (Datan_seq x)) N).
+Proof.
+assert (Tool : forall N, (-1) ^ (S (2 * N))  = - 1).
+ intro n ; induction n.
+  simpl ; field.
+  replace ((-1) ^ S (2 * S n)) with ((-1) ^ 2 * (-1) ^ S (2*n)).
+  rewrite IHn ; field.
+  rewrite <- pow_add.
+  replace (2 + S (2 * n))%nat with (S (2 * S n))%nat.
+  reflexivity.
+  intuition.
+intros N x x_lb x_ub.
+ induction N.
+  unfold Datan_seq, Ratan_seq, tg_alt ; simpl.
+  intros eps eps_pos.
+   elim (derivable_pt_lim_id x eps eps_pos) ; intros delta Hdelta ; exists delta.
+   intros h hneq h_b.
+    replace (1 * ((x + h) * 1 / 1) - 1 * (x * 1 / 1)) with (id (x + h) - id x). 
+    rewrite Rmult_1_r.
+    apply Hdelta ; assumption.
+    unfold id ; field ; assumption.
+  intros eps eps_pos.
+  assert (eps_3_pos : (eps/3) > 0) by fourier.
+  elim (IHN (eps/3) eps_3_pos) ; intros delta1 Hdelta1.
+  assert (Main : derivable_pt_lim (fun x : R =>tg_alt (Ratan_seq x) (S N)) x ((tg_alt (Datan_seq x)) (S N))).
+   clear -Tool ; intros eps' eps'_pos.
+   elim (derivable_pt_lim_pow x (2 * (S N) + 1) eps' eps'_pos) ; intros delta Hdelta ; exists delta.
+   intros h h_neq h_b ; unfold tg_alt, Ratan_seq, Datan_seq.
+   replace (((-1) ^ S N * ((x + h) ^ (2 * S N + 1) / INR (2 * S N + 1)) -
+    (-1) ^ S N * (x ^ (2 * S N + 1) / INR (2 * S N + 1))) / h -
+    (-1) ^ S N * x ^ (2 * S N)) 
+    with (((-1)^(S N)) * ((((x + h) ^ (2 * S N + 1) / INR (2 * S N + 1)) -
+    (x ^ (2 * S N + 1) / INR (2 * S N + 1))) / h - x ^ (2 * S N))).
+   rewrite Rabs_mult ; rewrite pow_1_abs ; rewrite Rmult_1_l.
+   replace (((x + h) ^ (2 * S N + 1) / INR (2 * S N + 1) -
+    x ^ (2 * S N + 1) / INR (2 * S N + 1)) / h - x ^ (2 * S N))
+    with ((/INR (2* S N + 1)) * (((x + h) ^ (2 * S N + 1) - x ^ (2 * S N + 1)) / h -
+    INR (2 * S N + 1) * x ^ pred (2 * S N + 1))).
+   rewrite Rabs_mult.
+   case (Req_dec (((x + h) ^ (2 * S N + 1) - x ^ (2 * S N + 1)) / h -
+     INR (2 * S N + 1) * x ^ pred (2 * S N + 1)) 0) ; intro Heq.
+   rewrite Heq ; rewrite Rabs_R0 ; rewrite Rmult_0_r ; assumption.
+   apply Rlt_trans with (r2:=Rabs
+           (((x + h) ^ (2 * S N + 1) - x ^ (2 * S N + 1)) / h -
+            INR (2 * S N + 1) * x ^ pred (2 * S N + 1))).
+   rewrite <- Rmult_1_l ; apply Rmult_lt_compat_r.
+   apply Rabs_pos_lt ; assumption.
+   rewrite Rabs_right.
+   replace 1 with (/1) by field.
+   apply Rinv_1_lt_contravar ; intuition.
+   apply Rgt_ge ; replace (INR (2 * S N + 1)) with (INR (2*S N) + 1) ;
+   [apply RiemannInt.RinvN_pos | ].
+   replace (2 * S N + 1)%nat with (S (2 * S N))%nat by intuition ;
+   rewrite S_INR ; reflexivity.
+   apply Hdelta ; assumption.
+   rewrite Rmult_minus_distr_l.
+   replace (/ INR (2 * S N + 1) * (INR (2 * S N + 1) * x ^ pred (2 * S N + 1))) with (x ^ (2 * S N)).
+   unfold Rminus ; rewrite Rplus_comm.
+   replace (((x + h) ^ (2 * S N + 1) / INR (2 * S N + 1) +
+      - (x ^ (2 * S N + 1) / INR (2 * S N + 1))) / h + - x ^ (2 * S N))
+      with (- x ^ (2 * S N) + (((x + h) ^ (2 * S N + 1) / INR (2 * S N + 1) +
+      - (x ^ (2 * S N + 1) / INR (2 * S N + 1))) / h)) by intuition.
+   apply Rplus_eq_compat_l. field.
+   split ; [apply Rgt_not_eq|] ; intuition.
+   clear ; replace (pred (2 * S N + 1)) with (2 * S N)%nat by intuition.
+   field ; apply Rgt_not_eq ; intuition.
+   field ; split ; [apply Rgt_not_eq |] ; intuition.
+   elim (Main (eps/3) eps_3_pos) ; intros delta2 Hdelta2.
+   destruct delta1 as (delta1, delta1_pos) ; destruct delta2 as (delta2, delta2_pos).
+   pose (mydelta := Rmin delta1 delta2).
+   assert (mydelta_pos : mydelta > 0).
+    unfold mydelta ; rewrite Rmin_Rgt ; split ; assumption.
+   pose (delta := mkposreal mydelta mydelta_pos) ; exists delta ; intros h h_neq h_b.
+   clear Main IHN.
+   unfold Rminus at 1.
+   apply Rle_lt_trans with (r2:=eps/3 + eps / 3).
+   assert (Temp : (sum_f_R0 (tg_alt (Ratan_seq (x + h))) (S N) -
+    sum_f_R0 (tg_alt (Ratan_seq x)) (S N)) / h +
+    - sum_f_R0 (tg_alt (Datan_seq x)) (S N) = ((sum_f_R0 (tg_alt (Ratan_seq (x + h))) N -
+              sum_f_R0 (tg_alt (Ratan_seq x)) N) / h) + (-
+             sum_f_R0 (tg_alt (Datan_seq x)) N) + ((tg_alt (Ratan_seq (x + h)) (S N) - tg_alt (Ratan_seq x) (S N)) /
+             h - tg_alt (Datan_seq x) (S N))).
+    simpl ; field ; intuition.
+   apply Rle_trans with (r2:= Rabs ((sum_f_R0 (tg_alt (Ratan_seq (x + h))) N -
+        sum_f_R0 (tg_alt (Ratan_seq x)) N) / h +
+       - sum_f_R0 (tg_alt (Datan_seq x)) N) +
+       Rabs ((tg_alt (Ratan_seq (x + h)) (S N) - tg_alt (Ratan_seq x) (S N)) / h -
+        tg_alt (Datan_seq x) (S N))).
+   rewrite Temp ; clear Temp ; apply Rabs_triang.
+   apply Rplus_le_compat ; apply Rlt_le ; [apply Hdelta1 | apply Hdelta2] ;
+   intuition ; apply Rlt_le_trans with (r2:=delta) ; intuition unfold delta, mydelta.
+   apply Rmin_l.
+   apply Rmin_r.
+   fourier.
+Qed.
+
+Lemma Ratan_CVU' :
+  CVU (fun N x => sum_f_R0 (tg_alt (Ratan_seq x)) N)
+                     ps_atan (/2) (mkposreal (/2) pos_half_prf).
+Proof.
+apply (Alt_CVU (fun i r => Ratan_seq r i) ps_atan PI_tg (/2) pos_half);
+  lazy beta.
+    now intros; apply Ratan_seq_decreasing, Boule_half_to_interval.
+   now intros; apply Ratan_seq_converging, Boule_half_to_interval.
+  intros x b; apply Boule_half_to_interval in b.
+  unfold ps_atan; destruct (in_int x) as [inside | outside];
+   [ | destruct b; case outside; split; fourier].
+  destruct (ps_atan_exists_1 x inside) as [v Pv].
+  apply Un_cv_ext with (2 := Pv);[reflexivity].
+ intros x n b; apply Boule_half_to_interval in b.
+ rewrite <- (Rmult_1_l (PI_tg n)); unfold Ratan_seq, PI_tg. 
+ apply Rmult_le_compat_r.
+  apply Rlt_le, Rinv_0_lt_compat, (lt_INR 0); omega.
+ rewrite <- (pow1 (2 * n + 1)); apply pow_incr; assumption.
+exact PI_tg_cv.
+Qed.
+
+Lemma Ratan_CVU :
+  CVU (fun N x => sum_f_R0 (tg_alt (Ratan_seq x)) N)
+                     ps_atan 0  (mkposreal 1 Rlt_0_1).
+Proof.
+intros eps ep; destruct (Ratan_CVU' eps ep) as [N Pn].
+exists N; intros n x nN b_y.
+case (Rtotal_order 0 x) as [xgt0 | [x0 | x0]].
+  assert (Boule (/2) {| pos := / 2; cond_pos := pos_half_prf|} x).
+   revert b_y; unfold Boule; simpl; intros b_y; apply Rabs_def2 in b_y.
+   destruct b_y; unfold Boule; simpl; apply Rabs_def1; fourier.
+  apply Pn; assumption.
+ rewrite <- x0, ps_atan0_0.
+ rewrite <- (sum_eq (fun _ => 0)), sum_cte, Rmult_0_l, Rminus_0_r, Rabs_pos_eq.
+   assumption.
+  apply Rle_refl.
+ intros i _; unfold tg_alt, Ratan_seq, Rdiv; rewrite plus_comm; simpl.
+ solve[rewrite !Rmult_0_l, Rmult_0_r; auto].
+replace (ps_atan x - sum_f_R0 (tg_alt (Ratan_seq x)) n) with
+  (-(ps_atan (-x) - sum_f_R0 (tg_alt (Ratan_seq (-x))) n)).
+ rewrite Rabs_Ropp.
+ assert (Boule (/2) {| pos := / 2; cond_pos := pos_half_prf|} (-x)).
+  revert b_y; unfold Boule; simpl; intros b_y; apply Rabs_def2 in b_y.
+  destruct b_y; unfold Boule; simpl; apply Rabs_def1; fourier.
+ apply Pn; assumption.
+unfold Rminus; rewrite ps_atan_opp, Ropp_plus_distr, sum_Ratan_seq_opp.
+rewrite !Ropp_involutive; reflexivity.
+Qed.
+
+Lemma Alt_PI_tg : forall n, PI_tg n = Ratan_seq 1 n.
+Proof.
+intros n; unfold PI_tg, Ratan_seq, Rdiv; rewrite pow1, Rmult_1_l.
+reflexivity.
+Qed.
+
+Lemma Ratan_is_ps_atan : forall eps, eps > 0 ->
+       exists N, forall n, (n >= N)%nat -> forall x, -1 < x -> x < 1 ->
+       Rabs (sum_f_R0 (tg_alt (Ratan_seq x)) n - ps_atan x) < eps.
+Proof.
+intros eps ep.
+destruct (Ratan_CVU _ ep) as [N1 PN1].
+exists N1; intros n nN x xm1 x1; rewrite <- Rabs_Ropp, Ropp_minus_distr.
+apply PN1; [assumption | ].
+unfold Boule; simpl; rewrite Rminus_0_r; apply Rabs_def1; assumption.
+Qed.
+
+Lemma Datan_continuity : continuity (fun x => /(1+x ^ 2)).
+Proof.
+apply continuity_inv.
+apply continuity_plus.
+apply continuity_const ; unfold constant ; intuition.
+apply derivable_continuous ; apply derivable_pow.
+intro x ; apply Rgt_not_eq ; apply Rge_gt_trans with (1+0) ; [|fourier] ;
+ apply Rplus_ge_compat_l.
+ replace (x^2) with (x²).
+ apply Rle_ge ; apply Rle_0_sqr.
+ unfold Rsqr ; field.
+Qed.
+
+Lemma derivable_pt_lim_ps_atan : forall x, -1 < x < 1 ->
+  derivable_pt_lim ps_atan x ((fun y => /(1 + y ^ 2)) x).
+Proof.
+intros x x_encad.
+destruct (boule_in_interval (-1) 1 x x_encad) as [c [r [Pcr1 [P1 P2]]]].
+change (/ (1 + x ^ 2)) with ((fun u => /(1 + u ^ 2)) x).
+assert (t := derivable_pt_lim_CVU).
+apply derivable_pt_lim_CVU with 
+          (fn := (fun N x => sum_f_R0 (tg_alt (Ratan_seq x)) N))
+          (fn' := (fun N x => sum_f_R0 (tg_alt (Datan_seq x)) N))
+          (c := c) (r := r).
+    assumption.
+   intros y N inb; apply Rabs_def2 in inb; destruct inb.
+   apply Datan_is_datan.
+    fourier.
+   fourier.
+  intros y inb; apply Rabs_def2 in inb; destruct inb.
+  assert (y_gt_0 : -1 < y) by fourier.
+  assert (y_lt_1 : y < 1) by fourier.
+  intros eps eps_pos ; elim (Ratan_is_ps_atan eps eps_pos).
+  intros N HN ; exists N; intros n n_lb ; apply HN ; tauto.
+ apply Datan_CVU_prelim.
+ replace ((c - r + (c + r)) / 2) with c by field.
+ unfold mkposreal_lb_ub; simpl.
+ replace ((c + r - (c - r)) / 2) with (r :R) by field.
+ assert (Rabs c < 1 - r).
+  unfold Boule in Pcr1; destruct r; simpl in *; apply Rabs_def1;
+  apply Rabs_def2 in Pcr1; destruct Pcr1; fourier.
+ fourier.
+intros; apply Datan_continuity.
+Qed.
+
+Lemma derivable_pt_ps_atan :
+   forall x, -1 < x < 1 -> derivable_pt ps_atan x.
+Proof.
+intros x x_encad.
+exists (/(1+x^2)) ; apply derivable_pt_lim_ps_atan; assumption.
+Qed.
+
+Lemma ps_atan_continuity_pt_1 : forall eps : R,
+       eps > 0 ->
+       exists alp : R,
+       alp > 0 /\
+       (forall x, x < 1 -> 0 < x -> R_dist x 1 < alp ->
+       dist R_met (ps_atan x) (Alt_PI/4) < eps).
+Proof.
+intros eps eps_pos.
+assert (eps_3_pos : eps / 3 > 0) by fourier.
+elim (Ratan_is_ps_atan (eps / 3) eps_3_pos) ; intros N1 HN1.
+unfold Alt_PI.
+destruct exist_PI as [v Pv]; replace ((4 * v)/4) with v by field.
+assert (Pv' : Un_cv (sum_f_R0 (tg_alt (Ratan_seq 1))) v).
+ apply Un_cv_ext with (2:= Pv).
+ intros; apply sum_eq; intros; unfold tg_alt; rewrite Alt_PI_tg; tauto.
+destruct (Pv' (eps / 3) eps_3_pos) as [N2 HN2].
+set (N := (N1 + N2)%nat).
+assert (O_lb : 0 <= 1) by intuition ; assert (O_ub : 1 <= 1) by intuition ;
+ elim (ps_atanSeq_continuity_pt_1 N 1 O_lb O_ub (eps / 3) eps_3_pos) ; intros alpha Halpha ;
+ clear -HN1 HN2 Halpha eps_3_pos; destruct Halpha as (alpha_pos, Halpha).
+exists alpha ; split;[assumption | ].
+intros x x_ub x_lb x_bounds.
+simpl ; unfold R_dist.
+replace (ps_atan x - v) with ((ps_atan x - sum_f_R0 (tg_alt (Ratan_seq x)) N)
+     + (sum_f_R0 (tg_alt (Ratan_seq x)) N - sum_f_R0 (tg_alt (Ratan_seq 1)) N)
+     + (sum_f_R0 (tg_alt (Ratan_seq 1)) N - v)).
+apply Rle_lt_trans with (r2:=Rabs (ps_atan x - sum_f_R0 (tg_alt (Ratan_seq x)) N) +
+      Rabs ((sum_f_R0 (tg_alt (Ratan_seq x)) N - sum_f_R0 (tg_alt (Ratan_seq 1)) N) +
+   (sum_f_R0 (tg_alt (Ratan_seq 1)) N - v))).
+rewrite Rplus_assoc ; apply Rabs_triang.
+   replace eps with (2 / 3 * eps + eps / 3).
+   rewrite Rplus_comm.
+   apply Rplus_lt_compat.
+   apply Rle_lt_trans with (r2 := Rabs (sum_f_R0 (tg_alt (Ratan_seq x)) N - sum_f_R0 (tg_alt (Ratan_seq 1)) N) +
+      Rabs (sum_f_R0 (tg_alt (Ratan_seq 1)) N - v)).
+   apply Rabs_triang.
+   apply Rlt_le_trans with (r2:= eps / 3 + eps / 3).
+   apply Rplus_lt_compat.
+   simpl in Halpha ; unfold R_dist in Halpha.
+   apply Halpha ; split.
+   unfold D_x, no_cond ; split ; [ | apply Rgt_not_eq ] ; intuition.
+   intuition.
+   apply HN2; unfold N; omega.
+   fourier.
+  rewrite <- Rabs_Ropp, Ropp_minus_distr; apply HN1.
+     unfold N; omega.  
+    fourier.
+  assumption.
+ field.
+ring.
+Qed.
+
+Lemma Datan_eq_DatanSeq_interv : forall x, -1 < x < 1 ->
+ forall (Pratan:derivable_pt ps_atan x) (Prmymeta:derivable_pt atan x),
+      derive_pt ps_atan x Pratan = derive_pt atan x Prmymeta.
+Proof.
+assert (freq : 0 < tan 1) by apply (Rlt_trans _ _ _ Rlt_0_1 tan_1_gt_1).
+intros x x_encad Pratan Prmymeta.
+ rewrite pr_nu_var2_interv with (g:=ps_atan) (lb:=-1) (ub:=tan 1)
+   (pr2 := derivable_pt_ps_atan x x_encad).
+ rewrite pr_nu_var2_interv with (f:=atan) (g:=atan) (lb:=-1) (ub:= 1) (pr2:=derivable_pt_atan x).
+ assert (Temp := derivable_pt_lim_ps_atan x x_encad).
+ assert (Hrew1 : derive_pt ps_atan x (derivable_pt_ps_atan x x_encad) = (/(1+x^2))).
+  apply derive_pt_eq_0 ; assumption.
+  rewrite derive_pt_atan.
+  rewrite Hrew1.
+  replace (Rsqr x) with (x ^ 2) by (unfold Rsqr; ring).
+  unfold Rdiv; rewrite Rmult_1_l; reflexivity.
+     fourier.
+    assumption.
+   intros; reflexivity.
+  fourier.
+ assert (t := tan_1_gt_1); split;destruct x_encad; fourier.
+intros; reflexivity.
+Qed.
+
+Lemma atan_eq_ps_atan :
+ forall x, 0 < x < 1 -> atan x = ps_atan x.
+Proof.
+intros x x_encad.
+assert (pr1 : forall c : R, 0 < c < x -> derivable_pt (atan - ps_atan) c).
+ intros c c_encad.
+ apply derivable_pt_minus.
+  exact (derivable_pt_atan c).
+ apply derivable_pt_ps_atan.
+  destruct x_encad; destruct c_encad; split; fourier.
+assert (pr2 : forall c : R, 0 < c < x -> derivable_pt id c).
+ intros ; apply derivable_pt_id; fourier.
+assert (delta_cont : forall c : R, 0 <= c <= x -> continuity_pt (atan - ps_atan) c).
+ intros c [[c_encad1 | c_encad1 ] [c_encad2 | c_encad2]];
+        apply continuity_pt_minus.
+        apply derivable_continuous_pt ; apply derivable_pt_atan. 
+       apply derivable_continuous_pt ; apply derivable_pt_ps_atan.
+       split; destruct x_encad; fourier.
+      apply derivable_continuous_pt, derivable_pt_atan.
+     apply derivable_continuous_pt, derivable_pt_ps_atan.
+     subst c; destruct x_encad; split; fourier.
+    apply derivable_continuous_pt, derivable_pt_atan.
+   apply derivable_continuous_pt, derivable_pt_ps_atan.
+   subst c; split; fourier.
+  apply derivable_continuous_pt, derivable_pt_atan.
+ apply derivable_continuous_pt, derivable_pt_ps_atan.
+ subst c; destruct x_encad; split; fourier.
+assert (id_cont : forall c : R, 0 <= c <= x -> continuity_pt id c).
+    intros ; apply derivable_continuous ; apply derivable_id.
+assert (x_lb : 0 < x) by (destruct x_encad; fourier).
+elim (MVT (atan - ps_atan)%F id 0 x pr1 pr2 x_lb delta_cont id_cont) ; intros d Temp ; elim Temp ; intros d_encad Main.
+clear - Main x_encad.
+assert (Temp : forall (pr: derivable_pt (atan - ps_atan) d), derive_pt (atan - ps_atan) d pr = 0).
+ intro pr.
+ assert (d_encad3 : -1 < d < 1).
+  destruct d_encad; destruct x_encad; split; fourier.
+ pose (pr3 := derivable_pt_minus atan ps_atan d (derivable_pt_atan d) (derivable_pt_ps_atan d d_encad3)).
+ rewrite <- pr_nu_var2_interv with (f:=(atan - ps_atan)%F) (g:=(atan - ps_atan)%F) (lb:=0) (ub:=x) (pr1:=pr3) (pr2:=pr).
+    unfold pr3. rewrite derive_pt_minus.
+    rewrite Datan_eq_DatanSeq_interv with (Prmymeta := derivable_pt_atan d).
+     intuition.
+    assumption. 
+   destruct d_encad; fourier.
+  assumption.
+ reflexivity.
+assert (iatan0 : atan 0 = 0).
+ apply tan_is_inj.
+   apply atan_bound.
+  rewrite Ropp_div; assert (t := PI2_RGT_0); split; fourier.
+ rewrite tan_0, atan_right_inv; reflexivity.
+generalize Main; rewrite Temp, Rmult_0_r.
+replace ((atan - ps_atan)%F x) with (atan x - ps_atan x) by intuition.
+replace ((atan - ps_atan)%F 0) with (atan 0 - ps_atan 0) by intuition.
+rewrite iatan0, ps_atan0_0, !Rminus_0_r.
+replace (derive_pt id d (pr2 d d_encad)) with 1. 
+ rewrite Rmult_1_r.
+ solve[intros M; apply Rminus_diag_uniq; auto].
+rewrite pr_nu_var with (g:=id) (pr2:=derivable_pt_id d).
+ symmetry ; apply derive_pt_id.
+tauto.
+Qed.
+
+
+Theorem Alt_PI_eq : Alt_PI = PI.
+apply Rmult_eq_reg_r with (/4); fold (Alt_PI/4); fold (PI/4);
+  [ | apply Rgt_not_eq; fourier].
+assert (0 < PI/6) by (apply PI6_RGT_0).
+assert (t1:= PI2_1).
+assert (t2 := PI_4).
+assert (m := Alt_PI_RGT_0).
+assert (-PI/2 < 1 < PI/2) by (rewrite Ropp_div; split; fourier).
+apply cond_eq; intros eps ep.
+change (R_dist (Alt_PI/4) (PI/4) < eps).
+assert (ca : continuity_pt atan 1).
+  apply derivable_continuous_pt, derivable_pt_atan.
+assert (Xe : exists eps', exists eps'',
+  eps' + eps'' <= eps /\ 0 < eps' /\ 0 < eps'').
+ exists (eps/2); exists (eps/2); repeat apply conj; fourier.
+destruct Xe as [eps' [eps'' [eps_ineq [ep' ep'']]]].
+destruct (ps_atan_continuity_pt_1 _ ep') as [alpha [a0 Palpha]].
+destruct (ca _ ep'') as [beta [b0 Pbeta]].
+assert (Xa : exists a, 0 < a < 1 /\ R_dist a 1 < alpha /\
+                R_dist a 1 < beta).
+ exists (Rmax (/2) (Rmax (1 - alpha /2) (1 - beta /2))).
+ assert (/2 <= Rmax (/2) (Rmax (1 - alpha /2) (1 - beta /2))) by apply Rmax_l.
+ assert (Rmax (1 - alpha /2) (1 - beta /2) <=
+         Rmax (/2) (Rmax (1 - alpha /2) (1 - beta /2))) by apply Rmax_r.
+ assert ((1 - alpha /2) <= Rmax (1 - alpha /2) (1 - beta /2)) by apply Rmax_l.
+ assert ((1 - beta /2) <= Rmax (1 - alpha /2) (1 - beta /2)) by apply Rmax_r.
+ assert (Rmax (1 - alpha /2) (1 - beta /2) < 1)
+   by (apply Rmax_lub_lt; fourier).
+ split;[split;[ | apply Rmax_lub_lt]; fourier | ].
+ assert (0 <= 1 - Rmax (/ 2) (Rmax (1 - alpha / 2) (1 - beta / 2))).
+  assert (Rmax (/2) (Rmax (1 - alpha / 2) 
+            (1 - beta /2)) <= 1) by (apply Rmax_lub; fourier).
+  fourier.
+ split; unfold R_dist; rewrite <-Rabs_Ropp, Ropp_minus_distr,
+   Rabs_pos_eq;fourier.
+destruct Xa as [a [[Pa0 Pa1] [P1 P2]]].
+apply Rle_lt_trans with (1 := R_dist_tri _ _ (ps_atan a)).
+apply Rlt_le_trans with (2 := eps_ineq).
+apply Rplus_lt_compat.
+rewrite R_dist_sym; apply Palpha; assumption.
+rewrite <- atan_eq_ps_atan.
+ rewrite <- atan_1; apply (Pbeta a); auto.
+ split; [ | exact P2].
+split;[exact I | apply Rgt_not_eq; assumption].
+split; assumption.
+Qed.
+
+Lemma PI_ineq :
+  forall N : nat,
+    sum_f_R0 (tg_alt PI_tg) (S (2 * N)) <= PI / 4 <=
+    sum_f_R0 (tg_alt PI_tg) (2 * N).
+Proof.
+intros; rewrite <- Alt_PI_eq; apply Alt_PI_ineq.
+Qed.
+
diff --git a/theories/Reals/vo.itarget b/theories/Reals/vo.itarget
index bcd47a0b2..d575c34c4 100644
--- a/theories/Reals/vo.itarget
+++ b/theories/Reals/vo.itarget
@@ -9,6 +9,7 @@ DiscrR.vo
 Exp_prop.vo
 Integration.vo
 LegacyRfield.vo
+Machin.vo
 MVT.vo
 NewtonInt.vo
 PartSum.vo
@@ -17,7 +18,9 @@ Ranalysis1.vo
 Ranalysis2.vo
 Ranalysis3.vo
 Ranalysis4.vo
+Ranalysis5.vo
 Ranalysis.vo
+Ratan.vo
 Raxioms.vo
 Rbase.vo
 Rbasic_fun.vo