adds general facts in the Reals library, whose need was detected in

experiments about computing PI

14 files changed, 782 insertions, 71 deletions

diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v
index e3c5298d7..71683193f 100644
--- a/theories/Reals/MVT.v
+++ b/theories/Reals/MVT.v
@@ -710,3 +710,32 @@ Proof.
     unfold constant_D_eq in H8; assert (H9 := H8 _ H2);
       unfold minus_fct in H9; rewrite <- H9; ring.
 Qed.
+
+(* A variant of MVT using absolute values. *)
+Lemma MVT_abs : 
+  forall (f f' : R -> R) (a b : R),
+  (forall c : R, Rmin a b <= c <= Rmax a b ->
+      derivable_pt_lim f c (f' c)) ->
+  exists c : R, Rabs (f b - f a) = Rabs (f' c) * Rabs (b - a) /\
+             Rmin a b <= c <= Rmax a b.
+Proof.
+intros f f' a b.
+destruct (Rle_dec a b) as [aleb | blta].
+ destruct (Req_dec a b) as [ab | anb].
+  unfold Rminus; intros _; exists a; split.
+   now rewrite <- ab, !Rplus_opp_r, Rabs_R0, Rmult_0_r.
+  split;[apply Rmin_l | apply Rmax_l].
+ rewrite Rmax_right, Rmin_left; auto; intros derv.
+ destruct (MVT_cor2 f f' a b) as [c [hc intc]];
+  [destruct aleb;[assumption | contradiction] | apply derv | ].
+ exists c; rewrite hc, Rabs_mult;split;
+  [reflexivity | unfold Rle; tauto].
+assert (b < a) by (apply Rnot_le_gt; assumption).
+assert (b <= a) by (apply Rlt_le; assumption).
+rewrite Rmax_left, Rmin_right; try assumption; intros derv.
+destruct (MVT_cor2 f f' b a) as [c [hc intc]];
+ [assumption | apply derv | ].
+exists c; rewrite <- Rabs_Ropp, Ropp_minus_distr, hc, Rabs_mult.
+split;[now rewrite <- (Rabs_Ropp (b - a)), Ropp_minus_distr| unfold Rle; tauto].
+Qed.
+
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index 1982d2dc8..ce65b5f2b 100644
--- a/theories/Reals/PSeries_reg.v
+++ b/theories/Reals/PSeries_reg.v
@@ -10,12 +10,116 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Ranalysis1.
+Require Import MVT.
 Require Import Max.
 Require Import Even.
+Require Import Fourier.
 Local Open Scope R_scope.
 
+(* Boule is French for Ball *)
+
 Definition Boule (x:R) (r:posreal) (y:R) : Prop := Rabs (y - x) < r.
 
+(* General properties of balls. *)
+
+Lemma Boule_convex : forall c d x y z,
+  Boule c d x -> Boule c d y -> x <= z <= y -> Boule c d z.
+intros c d x y z bx b_y intz.
+unfold Boule in bx, b_y; apply Rabs_def2 in bx;
+apply Rabs_def2 in b_y; apply Rabs_def1;
+ [apply Rle_lt_trans with (y - c);[apply Rplus_le_compat_r|]|
+  apply Rlt_le_trans with (x - c);[|apply Rplus_le_compat_r]];tauto.
+Qed.
+
+Definition boule_of_interval x y (h : x < y) :
+  {c :R & {r : posreal | c - r = x /\ c + r = y}}.
+exists ((x + y)/2).
+assert (radius : 0 < (y - x)/2).
+ unfold Rdiv; apply Rmult_lt_0_compat.
+  apply Rlt_Rminus; assumption.
+ now apply Rinv_0_lt_compat, Rlt_0_2.
+ 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].
+rewrite Rplus_comm; apply Rplus_lt_compat_l, Rmult_lt_compat_r.
+ apply Rinv_0_lt_compat, Rlt_0_2.
+apply Rlt_trans with z; assumption.
+destruct (boule_of_interval _ _ cmp) as [c [r [P1 P2]]].
+assert (0 < /2) by (apply Rinv_0_lt_compat, Rlt_0_2).
+exists c, r; split.
+ destruct h; unfold Boule; simpl; apply Rabs_def1.
+  apply Rplus_lt_reg_l with c; rewrite P2;
+  replace (c + (z - c)) with (z * / 2 + z * / 2) by field.
+  apply Rplus_lt_compat_l, Rmult_lt_compat_r;assumption.
+ apply Rplus_lt_reg_l with c; change (c + - r) with (c - r);
+ rewrite P1;
+ replace (c + (z - c)) with (z * / 2 + z * / 2) by field.
+ apply Rplus_lt_compat_r, Rmult_lt_compat_r;assumption.
+destruct h; split.
+ replace x with (x * / 2 + x * / 2) by field; rewrite P1.
+ apply Rplus_lt_compat_l, Rmult_lt_compat_r;assumption.
+replace y with (y * / 2 + y * /2) by field; rewrite P2.
+apply Rplus_lt_compat_r, Rmult_lt_compat_r;assumption.
+Qed.
+
+Lemma Ball_in_inter : forall c1 c2 r1 r2 x,
+  Boule c1 r1 x -> Boule c2 r2 x ->
+  {r3 : posreal | forall y, Boule x r3 y -> Boule c1 r1 y /\ Boule c2 r2 y}.
+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 as [_ u];
+  apply (fun h => Rplus_lt_reg_r _ _ _ (Rle_lt_trans _ _ _ h u)), Req_le; ring.
+assert (x < Rmin (c1 + r1) (c2 + r2)).
+ apply Rmin_glb_lt;[revert in1 | revert in2]; intros h;
+ apply Rabs_def2 in h; destruct h as [u _];
+ apply (fun h => Rplus_lt_reg_r _ _ _ (Rlt_le_trans _ _ _ u h)), Req_le; ring.
+assert (t: 0 < Rmin (x - Rmax (c1 - r1) (c2 - r2))
+              (Rmin (c1 + r1) (c2 + r2) - x)).
+ apply Rmin_glb_lt; apply Rlt_Rminus; assumption.
+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 as [h h'].
+apply Rmin_Rgt in h; destruct h as [cmp1 cmp2].
+apply Rplus_lt_reg_r in cmp2; apply Rmin_Rgt in cmp2.
+rewrite Ropp_Rmin, Ropp_minus_distr in h'.
+apply Rmax_Rlt in h'; destruct h' as [cmp3 cmp4];
+apply Rplus_lt_reg_r in cmp3; apply Rmax_Rlt in cmp3;
+split; apply Rabs_def1.
+apply (fun h => Rplus_lt_reg_l _ _ _ (Rle_lt_trans _ _ _ h (proj1 cmp2))), Req_le;
+ ring.
+apply (fun h => Rplus_lt_reg_l _ _ _ (Rlt_le_trans _ _ _ (proj1 cmp3) h)), Req_le;
+ ring.
+apply (fun h => Rplus_lt_reg_l _ _ _ (Rle_lt_trans _ _ _ h (proj2 cmp2))), Req_le;
+ ring.
+apply (fun h => Rplus_lt_reg_l _ _ _ (Rlt_le_trans _ _ _ (proj2 cmp3) h)), Req_le;
+ ring.
+Qed.
+
+Lemma Boule_center : forall x r, Boule x r x.
+Proof.
+intros x [r rpos]; unfold Boule, Rminus; simpl; rewrite Rplus_opp_r.
+rewrite Rabs_pos_eq;[assumption | apply Rle_refl].
+Qed.
+
 (** Uniform convergence *)
 Definition CVU (fn:nat -> R -> R) (f:R -> R) (x:R)
   (r:posreal) : Prop :=
@@ -258,3 +362,242 @@ Proof.
       rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rlt_0_1.
   apply Rplus_le_lt_0_compat; [ apply Rabs_pos | apply Rlt_0_1 ].
 Qed.
+
+(* Uniform convergence implies pointwise simple convergence *)
+Lemma CVU_cv : forall f g c d, CVU f g c d ->
+   forall x, Boule c d x -> Un_cv (fun n => f n x) (g x).
+intros f g c d cvu x bx eps ep; destruct (cvu eps ep) as [N Pn].
+ exists N; intros n nN; rewrite R_dist_sym; apply Pn; assumption.
+Qed.
+
+(* convergence is preserved through extensional equality *)
+Lemma CVU_ext_lim :
+  forall f g1 g2 c d, CVU f g1 c d -> (forall x, Boule c d x -> g1 x = g2 x) ->
+    CVU f g2 c d.
+intros f g1 g2 c d cvu q eps ep; destruct (cvu _ ep) as [N Pn].
+exists N; intros; rewrite <- q; auto.
+Qed.
+
+(* When a sequence of derivable functions converge pointwise towards
+  a function g, with the derivatives converging uniformly towards
+  a function g', then the function g' is the derivative of g. *)
+
+Lemma CVU_derivable :
+  forall f f' g g' c d,
+   CVU f' g' c d ->
+   (forall x, Boule c d x -> Un_cv (fun n => f n x) (g x)) ->
+   (forall n x, Boule c d x -> derivable_pt_lim (f n) x (f' n x)) ->
+   forall x, Boule c d x -> derivable_pt_lim g x (g' x).
+intros f f' g g' c d cvu cvp dff' x bx.
+set (rho_ :=
+       fun n y =>
+           if Req_EM_T y x then
+              f' n x
+           else ((f n y - f n x)/ (y - x))).
+set (rho := fun y =>
+               if Req_EM_T y x then
+                  g' x
+               else (g y - g x)/(y - x)).
+assert (ctrho : forall n z, Boule c d z -> continuity_pt (rho_ n) z).
+ intros n z bz.
+ destruct (Req_EM_T x z) as [xz | xnz].
+  rewrite <- xz.
+  intros eps' ep'.
+  destruct (dff' n x bx eps' ep') as [alp Pa].
+  exists (pos alp);split;[apply cond_pos | ].
+  intros z'; unfold rho_, D_x, dist, R_met; simpl; intros [[_ xnz'] dxz'].
+   destruct (Req_EM_T z' x) as [abs | _].
+    case xnz'; symmetry; exact abs.
+   destruct (Req_EM_T x x) as [_ | abs];[ | case abs; reflexivity].
+  pattern z' at 1; replace z' with (x + (z' - x)) by ring.
+  apply Pa;[intros h; case xnz';
+    replace z' with (z' - x + x) by ring; rewrite h, Rplus_0_l;
+       reflexivity | exact dxz'].
+ destruct (Ball_in_inter c c d d z bz bz) as [delta Pd].
+ assert (dz :  0 < Rmin delta (Rabs (z - x))).
+  now apply Rmin_glb_lt;[apply cond_pos | apply Rabs_pos_lt; intros zx0; case xnz;
+                       replace z with (z - x + x) by ring; rewrite zx0, Rplus_0_l].
+ assert (t' : forall y : R,
+      R_dist y z < Rmin delta (Rabs (z - x)) ->
+      (fun z : R => (f n z - f n x) / (z - x)) y = rho_ n y).
+  intros y dyz; unfold rho_; destruct (Req_EM_T y x) as [xy | xny].
+   rewrite xy in dyz.
+   destruct (Rle_dec  delta (Rabs (z - x))).
+    rewrite Rmin_left, R_dist_sym in dyz; unfold R_dist in dyz; fourier.
+   rewrite Rmin_right, R_dist_sym in dyz; unfold R_dist in dyz;
+      [case (Rlt_irrefl _ dyz) |apply Rlt_le, Rnot_le_gt; assumption].
+  reflexivity.
+ apply (continuity_pt_locally_ext (fun z => (f n z - f n x)/(z - x))
+             (rho_ n) _ z dz t'); clear t'.
+ apply continuity_pt_div.
+   apply continuity_pt_minus.
+    apply derivable_continuous_pt; eapply exist; apply dff'; assumption.
+   apply continuity_pt_const; intro; intro; reflexivity.
+  apply continuity_pt_minus;
+   [apply derivable_continuous_pt; exists 1; apply derivable_pt_lim_id
+   | apply continuity_pt_const; intro; reflexivity].
+ intros zx0; case xnz; replace z with (z - x + x) by ring.
+ rewrite zx0, Rplus_0_l; reflexivity.
+assert (CVU rho_ rho c d ).
+ intros eps ep.
+ assert (ep8 : 0 < eps/8).
+  fourier.
+ destruct (cvu _ ep8) as [N Pn1].
+ assert (cauchy1 : forall n p, (N <= n)%nat -> (N <= p)%nat ->
+           forall z, Boule c d z -> Rabs (f' n z - f' p z) < eps/4).
+  intros n p nN pN z bz; replace (eps/4) with (eps/8 + eps/8) by field.
+  rewrite <- Rabs_Ropp.
+  replace (-(f' n z - f' p z)) with (g' z - f' n z - (g' z - f' p z)) by ring.
+  apply Rle_lt_trans with (1 := Rabs_triang _ _); rewrite Rabs_Ropp.
+  apply Rplus_lt_compat; apply Pn1; assumption.
+ assert (step_2 : forall n p, (N <= n)%nat -> (N <= p)%nat ->
+         forall y, Boule c d y -> x <> y ->
+         Rabs ((f n y - f n x)/(y - x) - (f p y - f p x)/(y - x)) < eps/4).
+  intros n p nN pN y b_y xny.
+  assert (mm0 : (Rmin x y = x /\ Rmax x y = y) \/ 
+                (Rmin x y = y /\ Rmax x y = x)).
+   destruct (Rle_dec x y) as [H | H].
+    rewrite Rmin_left, Rmax_right.
+      left; split; reflexivity.
+     assumption.
+    assumption.
+   rewrite Rmin_right, Rmax_left.
+     right; split; reflexivity.
+    apply Rlt_le, Rnot_le_gt; assumption.
+   apply Rlt_le, Rnot_le_gt; assumption.
+  assert (mm : Rmin x y < Rmax x y).
+   destruct mm0 as [[q1 q2] | [q1 q2]]; generalize (Rminmax x y); rewrite q1, q2.
+    intros h; destruct h;[ assumption| contradiction].
+   intros h; destruct h as [h | h];[assumption | rewrite h in xny; case xny; reflexivity].
+  assert (dm : forall z, Rmin x y <= z <= Rmax x y ->
+            derivable_pt_lim (fun x => f n x - f p x) z (f' n z - f' p z)).
+   intros z intz; apply derivable_pt_lim_minus.
+    apply dff'; apply Boule_convex with (Rmin x y) (Rmax x y);
+      destruct mm0 as [[q1 q2] | [q1 q2]]; revert intz; rewrite ?q1, ?q2; intros;
+     try assumption.
+   apply dff'; apply Boule_convex with (Rmin x y) (Rmax x y);
+      destruct mm0 as [[q1 q2] | [q1 q2]]; revert intz; rewrite ?q1, ?q2; intros;
+     try assumption.
+
+  replace ((f n y - f n x) / (y - x) - (f p y - f p x) / (y - x))
+    with (((f n y - f p y) - (f n x - f p x))/(y - x)) by
+    (field; intros yx0; case xny; replace y with (y - x + x) by ring;
+     rewrite yx0, Rplus_0_l; reflexivity).
+  destruct (MVT_cor2 (fun x => f n x - f p x) (fun x => f' n x - f' p x)
+             (Rmin x y) (Rmax x y) mm dm) as [z [Pz inz]].
+  destruct mm0 as [[q1 q2] | [q1 q2]].
+   replace ((f n y - f p y - (f n x - f p x))/(y - x)) with
+    ((f n (Rmax x y) - f p (Rmax x y) - (f  n (Rmin x y) - f p (Rmin x y)))/
+      (Rmax x y - Rmin x y)) by (rewrite q1, q2; reflexivity).
+   unfold Rdiv; rewrite Pz, Rmult_assoc, Rinv_r, Rmult_1_r.
+    apply cauchy1; auto.
+    apply Boule_convex with (Rmin x y) (Rmax x y);
+      revert inz; rewrite ?q1, ?q2; intros;
+     try assumption.
+    split; apply Rlt_le; tauto.
+   rewrite q1, q2; apply Rminus_eq_contra, not_eq_sym; assumption.
+  replace ((f n y - f p y - (f n x - f p x))/(y - x)) with
+    ((f n (Rmax x y) - f p (Rmax x y) - (f  n (Rmin x y) - f p (Rmin x y)))/
+      (Rmax x y - Rmin x y)).
+   unfold Rdiv; rewrite Pz, Rmult_assoc, Rinv_r, Rmult_1_r.
+    apply cauchy1; auto.
+    apply Boule_convex with (Rmin x y) (Rmax x y);
+     revert inz; rewrite ?q1, ?q2; intros;
+    try assumption; split; apply Rlt_le; tauto.
+   rewrite q1, q2; apply Rminus_eq_contra; assumption.
+  rewrite q1, q2; field; split; 
+    apply Rminus_eq_contra;[apply not_eq_sym |]; assumption.
+ assert (unif_ac :
+  forall n p, (N <= n)%nat -> (N <= p)%nat ->
+     forall y, Boule c d y ->
+       Rabs (rho_ n y - rho_ p y) <= eps/2).
+  intros n p nN pN y b_y.
+  destruct (Req_dec x y) as [xy | xny].
+   destruct (Ball_in_inter c c d d x bx bx) as [delta Pdelta].
+   destruct (ctrho n y b_y _ ep8) as [d' [dp Pd]].
+   destruct (ctrho p y b_y _ ep8) as [d2 [dp2 Pd2]].
+   assert (mmpos : 0 < (Rmin (Rmin d' d2) delta)/2).
+    apply Rmult_lt_0_compat; repeat apply Rmin_glb_lt; try assumption.
+     apply cond_pos.
+    apply Rinv_0_lt_compat, Rlt_0_2.
+   apply Rle_trans with (1 := R_dist_tri _ _ (rho_ n (y + Rmin (Rmin d' d2) delta/2))).
+   replace (eps/2) with (eps/8 + (eps/4 + eps/8)) by field.
+   apply Rplus_le_compat.
+    rewrite R_dist_sym; apply Rlt_le, Pd;split;[split;[exact I | ] | ].
+      apply Rminus_not_eq_right; rewrite Rplus_comm; unfold Rminus;
+      rewrite Rplus_assoc, Rplus_opp_r, Rplus_0_r; apply Rgt_not_eq; assumption.
+    simpl; unfold R_dist.
+    unfold Rminus; rewrite (Rplus_comm y), Rplus_assoc, Rplus_opp_r, Rplus_0_r.
+    rewrite Rabs_pos_eq;[ |apply Rlt_le; assumption ].
+    apply Rlt_le_trans with (Rmin (Rmin d' d2) delta);[fourier | ].
+    apply Rle_trans with (Rmin d' d2); apply Rmin_l.
+   apply Rle_trans with (1 := R_dist_tri _ _ (rho_ p (y + Rmin (Rmin d' d2) delta/2))).
+   apply Rplus_le_compat.
+    apply Rlt_le.
+    replace (rho_ n (y + Rmin (Rmin d' d2) delta / 2)) with
+          ((f n (y + Rmin (Rmin d' d2) delta / 2) - f n x)/
+            ((y + Rmin (Rmin d' d2) delta / 2) - x)).
+     replace (rho_ p (y + Rmin (Rmin d' d2) delta / 2)) with
+          ((f p (y + Rmin (Rmin d' d2) delta / 2) - f p x)/
+             ((y + Rmin (Rmin d' d2) delta / 2) - x)).
+      apply step_2; auto; try fourier.
+      assert (0 < pos delta) by (apply cond_pos).
+      apply Boule_convex with y (y + delta/2).
+        assumption.
+       destruct (Pdelta (y + delta/2)); auto.
+       rewrite xy; unfold Boule; rewrite Rabs_pos_eq; try fourier; auto.
+      split; try fourier.
+      apply Rplus_le_compat_l, Rmult_le_compat_r;[ | apply Rmin_r].
+       now apply Rlt_le, Rinv_0_lt_compat, Rlt_0_2.
+      apply Rminus_not_eq_right; rewrite xy; apply Rgt_not_eq; fourier.
+     unfold rho_.
+     destruct (Req_EM_T (y + Rmin (Rmin d' d2) delta/2) x) as [ymx | ymnx].
+      case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); fourier.
+     reflexivity.
+    unfold rho_.
+    destruct (Req_EM_T (y + Rmin (Rmin d' d2) delta / 2) x) as [ymx | ymnx].
+     case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); fourier.
+    reflexivity.
+   apply Rlt_le, Pd2; split;[split;[exact I | apply Rlt_not_eq; fourier] | ].
+   simpl; unfold R_dist.
+   unfold Rminus; rewrite (Rplus_comm y), Rplus_assoc, Rplus_opp_r, Rplus_0_r.
+   rewrite Rabs_pos_eq;[ | fourier].
+   apply Rlt_le_trans with (Rmin (Rmin d' d2) delta); [fourier |].
+   apply Rle_trans with (Rmin d' d2).
+    solve[apply Rmin_l].
+   solve[apply Rmin_r].
+  apply Rlt_le, Rlt_le_trans with (eps/4);[ | fourier].
+  unfold rho_; destruct (Req_EM_T y x); solve[auto].
+ assert (unif_ac' : forall p, (N <= p)%nat ->
+           forall y, Boule c d y -> Rabs (rho y - rho_ p y) < eps).
+  assert (cvrho : forall y, Boule c d y -> Un_cv (fun n => rho_ n y) (rho y)).
+   intros y b_y; unfold rho_, rho; destruct (Req_EM_T y x).
+    intros eps' ep'; destruct (cvu eps' ep') as [N2 Pn2].
+    exists N2; intros n nN2; rewrite R_dist_sym; apply Pn2; assumption.
+   apply CV_mult.
+    apply CV_minus.
+     apply cvp; assumption.
+    apply cvp; assumption.
+   intros eps' ep'; simpl; exists 0%nat; intros; rewrite R_dist_eq; assumption.
+  intros p pN y b_y.
+  replace eps with (eps/2 + eps/2) by field.
+  assert (ep2 : 0 < eps/2) by fourier.
+  destruct (cvrho y b_y _ ep2) as [N2 Pn2].
+  apply Rle_lt_trans with (1 := R_dist_tri _ _ (rho_ (max N N2) y)).
+  apply Rplus_lt_le_compat.
+   solve[rewrite R_dist_sym; apply Pn2, Max.le_max_r].
+  apply unif_ac; auto; solve [apply Max.le_max_l].
+ exists N; intros; apply unif_ac'; solve[auto].
+intros eps ep.
+destruct (CVU_continuity _ _ _ _ H ctrho x bx eps ep) as [delta [dp Pd]].
+exists (mkposreal _ dp); intros h hn0 dh.
+replace ((g (x + h) - g x) / h) with (rho (x + h)).
+ replace (g' x) with (rho x).
+  apply Pd; unfold D_x, no_cond;split;[split;[solve[auto] | ] | ].
+   intros xxh; case hn0; replace h with (x + h - x) by ring; rewrite <- xxh; ring.
+  simpl; unfold R_dist; replace (x + h - x) with h by ring; exact dh.
+ unfold rho; destruct (Req_EM_T x x) as [ _ | abs];[ | case abs]; reflexivity.
+unfold rho; destruct (Req_EM_T (x + h) x) as [abs | _];[ | ].
+ case hn0; replace h with (x + h - x) by ring; rewrite abs; ring.
+replace (x + h - x) with h by ring; reflexivity.
+Qed.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index cb75500d0..fc5017f71 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -711,7 +711,7 @@ Proof.
 Qed.
 
 (*********************************************************)
-(** ** Substraction                                      *)
+(** ** Subtraction                                      *)
 (*********************************************************)
 
 Lemma Rminus_0_r : forall r, r - 0 = r.
@@ -1370,6 +1370,11 @@ Proof.
   now rewrite Rplus_0_r.
 Qed.
 
+Lemma Rlt_Rminus : forall a b:R, a < b -> 0 < b - a.
+Proof.
+  intros a b; apply Rgt_minus.
+Qed.
+
 (**********)
 Lemma Rle_minus : forall r1 r2, r1 <= r2 -> r1 - r2 <= 0.
 Proof.
@@ -1399,6 +1404,9 @@ Proof.
   ring.
 Qed.
 
+Lemma Rminus_gt_0_lt : forall a b, 0 < b - a -> a < b.
+Proof. intro; intro; apply Rminus_gt. Qed.
+
 (**********)
 Lemma Rminus_le : forall r1 r2, r1 - r2 <= 0 -> r1 <= r2.
 Proof.
@@ -1980,6 +1988,10 @@ Proof.
   apply Rinv_le_contravar with (1 := H).
 Qed.
 
+Lemma Ropp_div : forall x y, -x/y = - (x / y).
+intros x y; unfold Rdiv; ring.
+Qed.
+
 Lemma double : forall r1, 2 * r1 = r1 + r1.
 Proof.
   intro; ring.
@@ -2053,6 +2065,29 @@ Proof.
   intros; elim (completeness E H H0); intros; split with x; assumption.
 Qed.
 
+Lemma Rdiv_lt_0_compat : forall a b, 0 < a -> 0 < b -> 0 < a/b.
+Proof. 
+intros; apply Rmult_lt_0_compat;[|apply Rinv_0_lt_compat]; assumption.
+Qed.
+
+Lemma Rdiv_plus_distr : forall a b c, (a + b)/c = a/c + b/c.
+intros a b c; apply Rmult_plus_distr_r.
+Qed.
+
+Lemma Rdiv_minus_distr : forall a b c, (a - b)/c = a/c - b/c.
+intros a b c; unfold Rminus, Rdiv; rewrite Rmult_plus_distr_r; ring.
+Qed.
+
+(* A test for equality function. *)
+Lemma Req_EM_T : forall r1 r2:R, {r1 = r2} + {r1 <> r2}.
+Proof.
+  intros; destruct (total_order_T r1 r2) as [[H|]|H].
+  - right; red; intros ->; elim (Rlt_irrefl r2 H).
+  - left; assumption.
+  - right; red; intros ->; elim (Rlt_irrefl r2 H).
+Qed.
+
+
 (*********************************************************)
 (** * Definitions of new types                           *)
 (*********************************************************)
@@ -2070,6 +2105,7 @@ Record negreal : Type := mknegreal {neg :> R; cond_neg : neg < 0}.
 Record nonzeroreal : Type := mknonzeroreal
   {nonzero :> R; cond_nonzero : nonzero <> 0}.
 
+
 (** Compatibility *)
 
 Notation prod_neq_R0 := Rmult_integral_contrapositive_currified (only parsing).
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index 19e111f23..92f2acd4f 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -94,6 +94,10 @@ Proof.
   intros; unfold Rsqr; apply sqrt_square; assumption.
 Qed.
 
+Lemma sqrt_pow2 : forall x, 0 <= x -> sqrt (x ^ 2) = x.
+intros; simpl; rewrite Rmult_1_r, sqrt_square; auto.
+Qed.
+
 Lemma sqrt_Rsqr_abs : forall x:R, sqrt (Rsqr x) = Rabs x.
 Proof.
   intro x; rewrite Rsqr_abs; apply sqrt_Rsqr; apply Rabs_pos.
@@ -517,3 +521,4 @@ Proof.
   reflexivity.
   reflexivity.
 Qed.
+
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 6afc20f5a..f24df53a7 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -77,6 +77,23 @@ Definition continuity f : Prop := forall x:R, continuity_pt f x.
 Arguments continuity_pt f%F x0%R.
 Arguments continuity f%F.
 
+Lemma continuity_pt_locally_ext :
+  forall f g a x, 0 < a -> (forall y, R_dist y x < a -> f y = g y) ->
+  continuity_pt f x -> continuity_pt g x.
+intros f g a x a0 q cf eps ep.
+destruct (cf eps ep) as [a' [a'p Pa']].
+exists (Rmin a a'); split.
+ unfold Rmin; destruct (Rle_dec a a').
+  assumption.
+ assumption.
+intros y cy; rewrite <- !q.
+  apply Pa'.
+  split;[| apply Rlt_le_trans with (Rmin a a');[ | apply Rmin_r]];tauto.
+ rewrite R_dist_eq; assumption.   
+apply Rlt_le_trans with (Rmin a a');[ | apply Rmin_l]; tauto.
+Qed.
+
+
 (**********)
 Lemma continuity_pt_plus :
   forall f1 f2 (x0:R),
@@ -477,6 +494,47 @@ Proof.
   auto with real.
 Qed.
 
+(* Extensionally equal functions have the same derivative. *)
+
+Lemma derivable_pt_lim_ext : forall f g x l, (forall z, f z = g z) -> 
+  derivable_pt_lim f x l -> derivable_pt_lim g x l.
+intros f g x l fg df e ep; destruct (df e ep) as [d pd]; exists d; intros h;
+rewrite <- !fg; apply pd.
+Qed.
+
+(* extensionally equal functions have the same derivative, locally. *)
+
+Lemma derivable_pt_lim_locally_ext : forall f g x a b l, 
+  a < x < b ->
+  (forall z, a < z < b -> f z = g z) ->
+  derivable_pt_lim f x l -> derivable_pt_lim g x l.
+intros f g x a b l axb fg df e ep.
+destruct (df e ep) as [d pd].
+assert (d'h : 0 < Rmin d (Rmin (b - x) (x - a))).
+ apply Rmin_pos;[apply cond_pos | apply Rmin_pos; apply Rlt_Rminus; tauto].
+exists (mkposreal _ d'h); simpl; intros h hn0 cmp.
+rewrite <- !fg;[ |assumption | ].
+  apply pd;[assumption |].
+ apply Rlt_le_trans with (1 := cmp), Rmin_l.
+assert (-h < x - a).
+ apply Rle_lt_trans with (1 := Rle_abs _).
+ rewrite Rabs_Ropp; apply Rlt_le_trans with (1 := cmp).
+ rewrite Rmin_assoc; apply Rmin_r.
+assert (h < b - x).
+ apply Rle_lt_trans with (1 := Rle_abs _).
+ apply Rlt_le_trans with (1 := cmp).
+ rewrite Rmin_comm, <- Rmin_assoc; apply Rmin_l.
+split.
+ apply (Rplus_lt_reg_l (- h)).
+ replace ((-h) + (x + h)) with x by ring.
+ apply (Rplus_lt_reg_r (- a)).
+ replace (((-h) + a) + - a) with (-h) by ring.
+ assumption.
+apply (Rplus_lt_reg_r (- x)).
+replace (x + h + - x) with h by ring.
+assumption.
+Qed.
+
 
 (***********************************)
 (** * derivability -> continuity   *)
@@ -639,6 +697,24 @@ Proof.
   unfold mult_real_fct, mult_fct, fct_cte; reflexivity.
 Qed.
 
+Lemma derivable_pt_lim_div_scal :
+  forall f x l a, derivable_pt_lim f x l ->
+     derivable_pt_lim (fun y => f y / a) x (l / a).
+intros f x l a df;
+  apply (derivable_pt_lim_ext (fun y => /a * f y)).
+ intros z; rewrite Rmult_comm; reflexivity.
+unfold Rdiv; rewrite Rmult_comm; apply derivable_pt_lim_scal; assumption.
+Qed.
+
+Lemma derivable_pt_lim_scal_right :
+  forall f x l a, derivable_pt_lim f x l ->
+     derivable_pt_lim (fun y => f y * a) x (l * a).
+intros f x l a df;
+  apply (derivable_pt_lim_ext (fun y => a * f y)).
+ intros z; rewrite Rmult_comm; reflexivity.
+unfold Rdiv; rewrite Rmult_comm; apply derivable_pt_lim_scal; assumption.
+Qed.
+
 Lemma derivable_pt_lim_id : forall x:R, derivable_pt_lim id x 1.
 Proof.
   intro; unfold derivable_pt_lim.
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v
index dd8e0dd52..2f097c4ae 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -13,6 +13,7 @@ Require Import Rtrigo1.
 Require Import Ranalysis1.
 Require Import Ranalysis3.
 Require Import Exp_prop.
+Require Import MVT.
 Local Open Scope R_scope.
 
 (**********)
@@ -398,3 +399,14 @@ Proof.
   intro; apply derive_pt_eq_0.
   apply derivable_pt_lim_sinh.
 Qed.
+
+Lemma sinh_lt : forall x y, x < y -> sinh x < sinh y.
+intros x y xy; destruct (MVT_cor2 sinh cosh x y xy) as [c [Pc _]].
+ intros; apply derivable_pt_lim_sinh.
+apply Rplus_lt_reg_l with (Ropp (sinh x)); rewrite Rplus_opp_l, Rplus_comm.
+unfold Rminus at 1 in Pc; rewrite Pc; apply Rmult_lt_0_compat;[ | ].
+ unfold cosh; apply Rmult_lt_0_compat;[|apply Rinv_0_lt_compat, Rlt_0_2].
+ now apply Rplus_lt_0_compat; apply exp_pos.
+now apply Rlt_Rminus; assumption.
+Qed.
+
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index f787aa630..9da220035 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -1037,62 +1037,6 @@ Definition mkposreal_lb_ub (x lb ub:R) (lb_lt_x:lb<x) (x_lt_ub:x<ub) : posreal.
 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)) ->
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index c189b0333..9de1bba35 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -262,6 +262,16 @@ Proof.
   intros; unfold Rmax; case (Rle_dec x y); intro; assumption.
 Qed.
 
+Lemma Rmax_Rlt : forall x y z, 
+  Rmax x y < z <-> x < z /\ y < z.
+Proof.
+intros x y z; split.
+ unfold Rmax; case (Rle_dec x y).
+  intros xy yz; split;[apply Rle_lt_trans with y|]; assumption.
+  intros xz xy; split;[|apply Rlt_trans with x;[apply Rnot_le_gt|]];assumption.
+ intros [h h']; apply Rmax_lub_lt; assumption.
+Qed.
+
 (*********)
 Lemma Rmax_neg : forall x y:R, x < 0 -> y < 0 -> Rmax x y < 0.
 Proof.
@@ -350,6 +360,13 @@ Qed.
 
 Definition RRle_abs := Rle_abs.
 
+Lemma Rabs_le : forall a b, -b <= a <= b -> Rabs a <= b.
+Proof.
+intros a b; unfold Rabs; case Rcase_abs.
+ intros _ [it _]; apply Ropp_le_cancel; rewrite Ropp_involutive; exact it.
+intros _ [_ it]; exact it.
+Qed.
+
 (*********)
 Lemma Rabs_pos_eq : forall x:R, 0 <= x -> Rabs x = x.
 Proof.
@@ -608,3 +625,51 @@ Proof.
   intros.
   now rewrite Rabs_Zabs.
 Qed.
+
+Lemma Ropp_Rmax : forall x y, - Rmax x y = Rmin (-x) (-y).
+intros x y; apply Rmax_case_strong.
+ now intros w; rewrite Rmin_left;[ | apply Rge_le, Ropp_le_ge_contravar].
+now intros w; rewrite Rmin_right; [ | apply Rge_le, Ropp_le_ge_contravar].
+Qed.
+
+Lemma Ropp_Rmin : forall x y, - Rmin x y = Rmax (-x) (-y).
+intros x y; apply Rmin_case_strong.
+ now intros w; rewrite Rmax_left;[ | apply Rge_le, Ropp_le_ge_contravar].
+now intros w; rewrite Rmax_right; [ | apply Rge_le, Ropp_le_ge_contravar].
+Qed.
+
+Lemma Rmax_assoc : forall a b c, Rmax a (Rmax b c) = Rmax (Rmax a b) c.
+Proof.
+intros a b c.
+unfold Rmax; destruct (Rle_dec b c); destruct (Rle_dec a b);
+  destruct (Rle_dec a c); destruct (Rle_dec b c); auto with real;
+  match goal with 
+  | id :  ~ ?x <= ?y, id2 : ?x <= ?z |- _ =>
+   case id; apply Rle_trans with z; auto with real
+  | id : ~ ?x <= ?y, id2 : ~ ?z <= ?x |- _ =>
+   case id; apply Rle_trans with z; auto with real
+  end.
+Qed.
+
+Lemma Rminmax : forall a b, Rmin a b <= Rmax a b.
+Proof.
+intros a b; destruct (Rle_dec a b).
+ rewrite Rmin_left, Rmax_right; assumption.
+now rewrite Rmin_right, Rmax_left; assumption ||
+  apply Rlt_le, Rnot_le_gt.
+Qed.
+
+Lemma Rmin_assoc : forall x y z, Rmin x (Rmin y z) =
+  Rmin (Rmin x y) z.
+Proof.
+intros a b c.
+unfold Rmin; destruct (Rle_dec b c); destruct (Rle_dec a b);
+  destruct (Rle_dec a c); destruct (Rle_dec b c); auto with real;
+  match goal with 
+  | id :  ~ ?x <= ?y, id2 : ?x <= ?z |- _ =>
+   case id; apply Rle_trans with z; auto with real
+  | id : ~ ?x <= ?y, id2 : ~ ?z <= ?x |- _ =>
+   case id; apply Rle_trans with z; auto with real
+  end.
+Qed.
+
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 9beee06c5..6e9a34ab4 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -520,6 +520,12 @@ Proof.
   apply Rle_trans with (Rabs y); [ apply Rabs_pos | exact H ].
 Qed.
 
+Lemma Rsqr_pow2 : forall x, Rsqr x = x ^ 2.
+Proof.
+intros; unfold Rsqr; simpl; rewrite Rmult_1_r; reflexivity.
+Qed.
+
+
 (*******************************)
 (** *       PowerRZ            *)
 (*******************************)
@@ -783,6 +789,13 @@ Proof.
   ring.
 Qed.
 
+Lemma R_dist_mult_l : forall a b c,
+  R_dist (a * b) (a * c) = Rabs a * R_dist b c.
+Proof.
+unfold R_dist. 
+intros a b c; rewrite <- Rmult_minus_distr_l, Rabs_mult; reflexivity.
+Qed.
+
 (*******************************)
 (** *     Infinite Sum          *)
 (*******************************)
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 0dc3329ee..fc3b9592f 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -394,6 +394,15 @@ Proof.
   red; intro; rewrite H6 in H; elim (Rlt_irrefl _ H).
 Qed.
 
+Lemma Riemann_integrable_ext :
+  forall f g a b, 
+    (forall x, Rmin a b <= x <= Rmax a b -> f x = g x) ->
+    Riemann_integrable f a b -> Riemann_integrable g a b.
+intros f g a b fg rif eps; destruct (rif eps) as [phi [psi [P1 P2]]].
+exists phi; exists psi;split;[ | assumption ].
+intros t intt; rewrite <- fg;[ | assumption].
+apply P1; assumption.
+Qed.
 (**********)
 Definition RiemannInt (f:R -> R) (a b:R) (pr:Riemann_integrable f a b) : R :=
   let (a,_) := RiemannInt_exists pr RinvN RinvN_cv in a.
@@ -991,14 +1000,6 @@ Proof.
       | discrR ].
 Qed.
 
-Lemma Req_EM_T : forall r1 r2:R, {r1 = r2} + {r1 <> r2}.
-Proof.
-  intros; destruct (total_order_T r1 r2) as [[H|]|H].
-  - right; red; intros ->; elim (Rlt_irrefl r2 H).
-  - left; assumption.
-  - right; red; intros ->; elim (Rlt_irrefl r2 H).
-Qed.
-
 (* L1([a,b]) is a vectorial space *)
 Lemma RiemannInt_P10 :
   forall (f g:R -> R) (a b l:R),
@@ -3217,3 +3218,38 @@ Proof.
           | assert (H0 := RiemannInt_P1 pr); rewrite (RiemannInt_P8 pr H0);
             rewrite (RiemannInt_P33 _ H0 H); ring ] ].
 Qed.
+
+(* RiemannInt *)
+Lemma RiemannInt_const_bound :
+  forall f a b l u (h : Riemann_integrable f a b), a <= b ->
+    (forall x, a < x < b -> l <= f x <= u) ->
+    l * (b - a) <= RiemannInt h <= u * (b - a).
+intros f a b l u ri ab intf.
+rewrite <- !(fun l => RiemannInt_P15 (RiemannInt_P14 a b l)).
+split; apply RiemannInt_P19; try assumption;
+ intros x intx; unfold fct_cte; destruct (intf x intx); assumption.
+Qed.
+
+Lemma Riemann_integrable_scal :
+  forall f a b k, 
+     Riemann_integrable f a b ->
+     Riemann_integrable (fun x => k * f x) a b.
+intros f a b k ri.
+apply Riemann_integrable_ext with
+   (f := fun x => 0 + k * f x).
+ intros; ring.
+apply (RiemannInt_P10 _ (RiemannInt_P14 _ _ 0) ri).
+Qed.
+
+Arguments Riemann_integrable_scal [f a b] k _ eps.
+
+Lemma Riemann_integrable_Ropp :
+  forall f a b, Riemann_integrable f a b -> 
+    Riemann_integrable (fun x => - f x) a b.
+intros ff a b h.
+apply Riemann_integrable_ext with (f := fun x => (-1) * ff x).
+intros; ring.
+apply Riemann_integrable_scal; assumption.
+Qed.
+
+Arguments Riemann_integrable_Ropp [f a b] _ eps.
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 2eb485188..9099ec057 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -20,8 +20,10 @@ Require Import Ranalysis1.
 Require Import Exp_prop.
 Require Import Rsqrt_def.
 Require Import R_sqrt.
+Require Import Sqrt_reg.
 Require Import MVT.
 Require Import Ranalysis4.
+Require Import Fourier.
 Local Open Scope R_scope.
 
 Lemma P_Rmin : forall (P:R -> Prop) (x y:R), P x -> P y -> P (Rmin x y).
@@ -701,3 +703,128 @@ Proof.
   ring.
   apply derivable_pt_lim_exp.
 Qed.
+
+(* added later. *)
+
+Lemma Rpower_mult_distr :  
+  forall x y z, 0 < x -> 0 < y ->
+   Rpower x z * Rpower y z = Rpower (x * y) z.
+intros x y z x0 y0; unfold Rpower.
+rewrite <- exp_plus, ln_mult, Rmult_plus_distr_l; auto.
+Qed.
+
+Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> Rpower a c <= Rpower b c. 
+Proof.
+intros [c0 | c0];
+ [ | intros; rewrite <- c0, !Rpower_O; [apply Rle_refl | |] ].
+  intros [a0 [ab|ab]].
+   left; apply exp_increasing.
+   now apply Rmult_lt_compat_l; auto; apply ln_increasing; fourier.
+  rewrite ab; apply Rle_refl.
+ apply Rlt_le_trans with a; tauto.
+tauto.
+Qed.
+
+(* arcsinh function *)
+
+Definition arcsinh x := ln (x + sqrt (x ^ 2 + 1)).
+
+Lemma arcsinh_sinh : forall x, arcsinh (sinh x) = x.
+intros x; unfold sinh, arcsinh.
+assert (Rminus_eq_0 : forall r, r - r = 0) by (intros; ring).
+pattern 1 at 5; rewrite <- exp_0, <- (Rminus_eq_0 x); unfold Rminus.
+rewrite exp_plus.
+match goal with |- context[sqrt ?a] => 
+  replace a with (((exp x + exp(-x))/2)^2) by field
+end.
+rewrite sqrt_pow2;
+ [|apply Rlt_le, Rmult_lt_0_compat;[apply Rplus_lt_0_compat; apply exp_pos |
+                            apply Rinv_0_lt_compat, Rlt_0_2]].
+match goal with |- context[ln ?a] => replace a with (exp x) by field end. 
+rewrite ln_exp; reflexivity.
+Qed.
+
+Lemma sinh_arcsinh x : sinh (arcsinh x) = x. 
+unfold sinh, arcsinh.
+assert (cmp : 0 < x + sqrt (x ^ 2 + 1)).
+ destruct (Rle_dec x 0).
+  replace (x ^ 2) with ((-x) ^ 2) by ring.
+  assert (sqrt ((- x) ^ 2) < sqrt ((-x)^2+1)).
+   apply sqrt_lt_1_alt.
+   split;[apply pow_le | ]; fourier.
+  pattern x at 1; replace x with (- (sqrt ((- x) ^ 2))).
+   assert (t:= sqrt_pos ((-x)^2)); fourier.
+  simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive;[reflexivity | fourier].
+  apply Rplus_lt_le_0_compat;[apply Rnot_le_gt; assumption | apply sqrt_pos].
+rewrite exp_ln;[ | assumption].
+rewrite exp_Ropp, exp_ln;[ | assumption].
+assert (Rmult_minus_distr_r :
+         forall x y z, (x - y) * z = x * z - y * z) by (intros; ring).
+apply Rminus_diag_uniq; unfold Rdiv; rewrite Rmult_minus_distr_r.
+assert (t: forall x y z, x - z = y -> x - y - z = 0);[ | apply t; clear t].
+ intros a b c H; rewrite <- H; ring.
+apply Rmult_eq_reg_l with (2 * (x + sqrt (x ^ 2 + 1)));[ |
+ apply Rgt_not_eq, Rmult_lt_0_compat;[apply Rlt_0_2 | assumption]].
+assert (pow2_sqrt : forall x, 0 <= x -> sqrt x ^ 2 = x) by
+ (intros; simpl; rewrite Rmult_1_r, sqrt_sqrt; auto).
+field_simplify;[rewrite pow2_sqrt;[field | ] | apply Rgt_not_eq; fourier].
+apply Rplus_le_le_0_compat;[simpl; rewrite Rmult_1_r; apply (Rle_0_sqr x)|apply Rlt_le, Rlt_0_1].
+Qed.
+
+Lemma derivable_pt_lim_arcsinh :
+  forall x, derivable_pt_lim arcsinh x (/sqrt (x ^ 2 + 1)).
+intros x; unfold arcsinh.
+assert (0 < x + sqrt (x ^ 2 + 1)).
+ destruct (Rle_dec x 0);
+  [ | assert (0 < x) by (apply Rnot_le_gt; assumption);
+    apply Rplus_lt_le_0_compat; auto; apply sqrt_pos].
+ replace (x ^ 2) with ((-x) ^ 2) by ring.
+ assert (sqrt ((- x) ^ 2) < sqrt ((-x)^2+1)).
+  apply sqrt_lt_1_alt.
+  split;[apply pow_le|]; fourier.
+ pattern x at 1; replace x with (- (sqrt ((- x) ^ 2))).
+  assert (t:= sqrt_pos ((-x)^2)); fourier.
+ simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive; auto; fourier.
+assert (0 < x ^ 2 + 1).
+ apply Rplus_le_lt_0_compat;[simpl; rewrite Rmult_1_r; apply Rle_0_sqr|fourier].
+replace (/sqrt (x ^ 2 + 1)) with
+ (/(x + sqrt (x ^ 2 + 1)) * 
+    (1 + (/(2 * sqrt (x ^ 2 + 1)) * (INR 2 * x ^ 1 + 0)))).
+apply (derivable_pt_lim_comp (fun x => x + sqrt (x ^ 2 + 1)) ln).
+ apply (derivable_pt_lim_plus).
+  apply derivable_pt_lim_id.
+   apply (derivable_pt_lim_comp (fun x => x ^ 2 + 1) sqrt x).
+    apply derivable_pt_lim_plus.
+     apply derivable_pt_lim_pow.
+    apply derivable_pt_lim_const.
+   apply derivable_pt_lim_sqrt; assumption.
+  apply derivable_pt_lim_ln; assumption.
+ replace (INR 2 * x ^ 1 + 0) with (2 * x) by (simpl; ring).
+replace (1 + / (2 * sqrt (x ^ 2 + 1)) * (2 * x)) with
+ (((sqrt (x ^ 2 + 1) + x))/sqrt (x ^ 2 + 1));
+ [ | field; apply Rgt_not_eq, sqrt_lt_R0; assumption].
+apply Rmult_eq_reg_l with (x + sqrt (x ^ 2 + 1));
+  [ | apply Rgt_not_eq; assumption].
+rewrite <- Rmult_assoc, Rinv_r;[field | ]; apply Rgt_not_eq; auto;
+  apply sqrt_lt_R0; assumption.
+Qed.
+
+Lemma arcsinh_lt : forall x y, x < y -> arcsinh x < arcsinh y.
+intros x y xy.
+case (Rle_dec (arcsinh y) (arcsinh x));[ | apply Rnot_le_lt ].
+intros abs; case (Rlt_not_le _ _ xy).
+rewrite <- (sinh_arcsinh y), <- (sinh_arcsinh x).
+destruct abs as [lt | q];[| rewrite q; fourier].
+apply Rlt_le, sinh_lt; assumption.
+Qed.
+
+Lemma arcsinh_le : forall x y, x <= y -> arcsinh x <= arcsinh y.
+intros x y [xy | xqy].
+ apply Rlt_le, arcsinh_lt; assumption.
+rewrite xqy; apply Rle_refl.
+Qed.
+
+Lemma arcsinh_0 : arcsinh 0 = 0.
+ unfold arcsinh; rewrite pow_ne_zero, !Rplus_0_l, sqrt_1, ln_1;
+  [reflexivity | discriminate].
+Qed.
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 57b9d3d2f..b3e297598 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -404,3 +404,26 @@ Proof.
   apply Rinv_neq_0_compat.
   assumption.
 Qed.
+
+(* Convergence is preserved after shifting the indices. *)
+Lemma CV_shift : 
+  forall f k l, Un_cv (fun n => f (n + k)%nat) l -> Un_cv f l.
+intros f' k l cvfk eps ep; destruct (cvfk eps ep) as [N Pn].
+exists (N + k)%nat; intros n nN; assert (tmp: (n = (n - k) + k)%nat).
+ rewrite Nat.sub_add;[ | apply le_trans with (N + k)%nat]; auto with arith.
+rewrite tmp; apply Pn; apply Nat.le_add_le_sub_r; assumption.
+Qed.
+
+Lemma CV_shift' : 
+  forall f k l, Un_cv f l -> Un_cv (fun n => f (n + k)%nat) l.
+intros f' k l cvf eps ep; destruct (cvf eps ep) as [N Pn].
+exists N; intros n nN; apply Pn; auto with arith.
+Qed.
+
+(* Growing property is preserved after shifting the indices (one way only) *)
+
+Lemma Un_growing_shift : 
+   forall k un, Un_growing un -> Un_growing (fun n => un (n + k)%nat).
+Proof.
+intros k un P n; apply P.
+Qed.
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 2e3d7f167..af6f2b3ec 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -450,6 +450,14 @@ Proof.
       assumption.
 Qed.
 
+(* A general purpose corollary. *)
+Lemma cv_pow_half : forall a, Un_cv (fun n => a/2^n) 0.
+intros a; unfold Rdiv; replace 0 with (a * 0) by ring.
+apply CV_mult.
+ intros eps ep; exists 0%nat; rewrite R_dist_eq; intros n _; assumption.
+exact (cv_infty_cv_R0 pow_2_n pow_2_n_neq_R0 pow_2_n_infty).
+Qed.
+
 (** Intermediate Value Theorem *)
 Lemma IVT :
   forall (f:R -> R) (x y:R),
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index ac15cf21e..e9423de6f 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -965,12 +965,6 @@ Proof.
     intros; exists (f0 x0); apply H4.
 Qed.
 
-Lemma Rlt_Rminus : forall a b:R, a < b -> 0 < b - a.
-Proof.
-  intros; apply Rplus_lt_reg_l with a; rewrite Rplus_0_r;
-    replace (a + (b - a)) with b; [ assumption | ring ].
-Qed.
-
 Lemma prolongement_C0 :
   forall (f:R -> R) (a b:R),
     a <= b ->