finish the rearrangement for removing the sin_PI2 axiom. This new version

- provides the atan function
- shows that this function is equal between -1 and 1 to a function defined
   with power series
- establishes the equality with the PI value as given by the alternated
  series constructed with PI_tg
- provides a smarter theorem to compute approximations of PI, based on a
  formula in the same family as the one used by John Machin in 1706

Dependencies between files have been rearranged so that the new theorems
are loaded with the library Reals.

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

1 files changed, 1 insertions, 772 deletions

diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v
index 01715cf3d..59c81457c 100644
--- a/theories/Reals/Ranalysis.v
+++ b/theories/Reals/Ranalysis.v
@@ -26,775 +26,4 @@ Require Export RList.
 Require Export Sqrt_reg.
 Require Export Ranalysis4.
 Require Export Rpower.
-Open Local Scope R_scope.
-
-Axiom AppVar : R.
-
-(**********)
-Ltac intro_hyp_glob trm :=
-  match constr:trm with
-    | (?X1 + ?X2)%F =>
-      match goal with
-        |  |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
-        |  |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
-        | _ => idtac
-      end
-    | (?X1 - ?X2)%F =>
-      match goal with
-        |  |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
-        |  |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
-        | _ => idtac
-      end
-    | (?X1 * ?X2)%F =>
-      match goal with
-        |  |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
-        |  |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
-        | _ => idtac
-      end
-    | (?X1 / ?X2)%F =>
-      let aux := constr:X2 in
-        match goal with
-          | _:(forall x0:R, aux x0 <> 0) |- (derivable _) =>
-            intro_hyp_glob X1; intro_hyp_glob X2
-          | _:(forall x0:R, aux x0 <> 0) |- (continuity _) =>
-            intro_hyp_glob X1; intro_hyp_glob X2
-          |  |- (derivable _) =>
-            cut (forall x0:R, aux x0 <> 0);
-              [ intro; intro_hyp_glob X1; intro_hyp_glob X2 | try assumption ]
-          |  |- (continuity _) =>
-            cut (forall x0:R, aux x0 <> 0);
-              [ intro; intro_hyp_glob X1; intro_hyp_glob X2 | try assumption ]
-          | _ => idtac
-        end
-    | (comp ?X1 ?X2) =>
-      match goal with
-        |  |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
-        |  |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
-        | _ => idtac
-      end
-    | (- ?X1)%F =>
-      match goal with
-        |  |- (derivable _) => intro_hyp_glob X1
-        |  |- (continuity _) => intro_hyp_glob X1
-        | _ => idtac
-      end
-    | (/ ?X1)%F =>
-      let aux := constr:X1 in
-        match goal with
-          | _:(forall x0:R, aux x0 <> 0) |- (derivable _) =>
-            intro_hyp_glob X1
-          | _:(forall x0:R, aux x0 <> 0) |- (continuity _) =>
-            intro_hyp_glob X1
-          |  |- (derivable _) =>
-            cut (forall x0:R, aux x0 <> 0);
-              [ intro; intro_hyp_glob X1 | try assumption ]
-          |  |- (continuity _) =>
-            cut (forall x0:R, aux x0 <> 0);
-              [ intro; intro_hyp_glob X1 | try assumption ]
-          | _ => idtac
-        end
-    | cos => idtac
-    | sin => idtac
-    | cosh => idtac
-    | sinh => idtac
-    | exp => idtac
-    | Rsqr => idtac
-    | sqrt => idtac
-    | id => idtac
-    | (fct_cte _) => idtac
-    | (pow_fct _) => idtac
-    | Rabs => idtac
-    | ?X1 =>
-      let p := constr:X1 in
-        match goal with
-          | _:(derivable p) |- _ => idtac
-          |  |- (derivable p) => idtac
-          |  |- (derivable _) =>
-            cut (True -> derivable p);
-              [ intro HYPPD; cut (derivable p);
-                [ intro; clear HYPPD | apply HYPPD; clear HYPPD; trivial ]
-                | idtac ]
-          | _:(continuity p) |- _ => idtac
-          |  |- (continuity p) => idtac
-          |  |- (continuity _) =>
-            cut (True -> continuity p);
-              [ intro HYPPD; cut (continuity p);
-                [ intro; clear HYPPD | apply HYPPD; clear HYPPD; trivial ]
-                | idtac ]
-          | _ => idtac
-        end
-  end.
-
-(**********)
-Ltac intro_hyp_pt trm pt :=
-  match constr:trm with
-    | (?X1 + ?X2)%F =>
-      match goal with
-        |  |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
-        |  |- (continuity_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
-        |  |- (derive_pt _ _ _ = _) =>
-          intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
-        | _ => idtac
-      end
-    | (?X1 - ?X2)%F =>
-      match goal with
-        |  |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
-        |  |- (continuity_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
-        |  |- (derive_pt _ _ _ = _) =>
-          intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
-        | _ => idtac
-      end
-    | (?X1 * ?X2)%F =>
-      match goal with
-        |  |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
-        |  |- (continuity_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
-        |  |- (derive_pt _ _ _ = _) =>
-          intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
-        | _ => idtac
-      end
-    | (?X1 / ?X2)%F =>
-      let aux := constr:X2 in
-        match goal with
-          | _:(aux pt <> 0) |- (derivable_pt _ _) =>
-            intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
-          | _:(aux pt <> 0) |- (continuity_pt _ _) =>
-            intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
-          | _:(aux pt <> 0) |- (derive_pt _ _ _ = _) =>
-            intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
-          | id:(forall x0:R, aux x0 <> 0) |- (derivable_pt _ _) =>
-            generalize (id pt); intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
-          | id:(forall x0:R, aux x0 <> 0) |- (continuity_pt _ _) =>
-            generalize (id pt); intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
-          | id:(forall x0:R, aux x0 <> 0) |- (derive_pt _ _ _ = _) =>
-            generalize (id pt); intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
-          |  |- (derivable_pt _ _) =>
-            cut (aux pt <> 0);
-              [ intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt | try assumption ]
-          |  |- (continuity_pt _ _) =>
-            cut (aux pt <> 0);
-              [ intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt | try assumption ]
-          |  |- (derive_pt _ _ _ = _) =>
-            cut (aux pt <> 0);
-              [ intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt | try assumption ]
-          | _ => idtac
-        end
-    | (comp ?X1 ?X2) =>
-      match goal with
-        |  |- (derivable_pt _ _) =>
-          let pt_f1 := eval cbv beta in (X2 pt) in
-            (intro_hyp_pt X1 pt_f1; intro_hyp_pt X2 pt)
-        |  |- (continuity_pt _ _) =>
-          let pt_f1 := eval cbv beta in (X2 pt) in
-            (intro_hyp_pt X1 pt_f1; intro_hyp_pt X2 pt)
-        |  |- (derive_pt _ _ _ = _) =>
-          let pt_f1 := eval cbv beta in (X2 pt) in
-            (intro_hyp_pt X1 pt_f1; intro_hyp_pt X2 pt)
-        | _ => idtac
-      end
-    | (- ?X1)%F =>
-      match goal with
-        |  |- (derivable_pt _ _) => intro_hyp_pt X1 pt
-        |  |- (continuity_pt _ _) => intro_hyp_pt X1 pt
-        |  |- (derive_pt _ _ _ = _) => intro_hyp_pt X1 pt
-        | _ => idtac
-      end
-    | (/ ?X1)%F =>
-      let aux := constr:X1 in
-        match goal with
-          | _:(aux pt <> 0) |- (derivable_pt _ _) =>
-            intro_hyp_pt X1 pt
-          | _:(aux pt <> 0) |- (continuity_pt _ _) =>
-            intro_hyp_pt X1 pt
-          | _:(aux pt <> 0) |- (derive_pt _ _ _ = _) =>
-            intro_hyp_pt X1 pt
-          | id:(forall x0:R, aux x0 <> 0) |- (derivable_pt _ _) =>
-            generalize (id pt); intro; intro_hyp_pt X1 pt
-          | id:(forall x0:R, aux x0 <> 0) |- (continuity_pt _ _) =>
-            generalize (id pt); intro; intro_hyp_pt X1 pt
-          | id:(forall x0:R, aux x0 <> 0) |- (derive_pt _ _ _ = _) =>
-            generalize (id pt); intro; intro_hyp_pt X1 pt
-          |  |- (derivable_pt _ _) =>
-            cut (aux pt <> 0); [ intro; intro_hyp_pt X1 pt | try assumption ]
-          |  |- (continuity_pt _ _) =>
-            cut (aux pt <> 0); [ intro; intro_hyp_pt X1 pt | try assumption ]
-          |  |- (derive_pt _ _ _ = _) =>
-            cut (aux pt <> 0); [ intro; intro_hyp_pt X1 pt | try assumption ]
-          | _ => idtac
-        end
-    | cos => idtac
-    | sin => idtac
-    | cosh => idtac
-    | sinh => idtac
-    | exp => idtac
-    | Rsqr => idtac
-    | id => idtac
-    | (fct_cte _) => idtac
-    | (pow_fct _) => idtac
-    | sqrt =>
-      match goal with
-        |  |- (derivable_pt _ _) => cut (0 < pt); [ intro | try assumption ]
-        |  |- (continuity_pt _ _) =>
-          cut (0 <= pt); [ intro | try assumption ]
-        |  |- (derive_pt _ _ _ = _) =>
-          cut (0 < pt); [ intro | try assumption ]
-        | _ => idtac
-      end
-    | Rabs =>
-      match goal with
-        |  |- (derivable_pt _ _) =>
-          cut (pt <> 0); [ intro | try assumption ]
-        | _ => idtac
-      end
-    | ?X1 =>
-      let p := constr:X1 in
-        match goal with
-          | _:(derivable_pt p pt) |- _ => idtac
-          |  |- (derivable_pt p pt) => idtac
-          |  |- (derivable_pt _ _) =>
-            cut (True -> derivable_pt p pt);
-              [ intro HYPPD; cut (derivable_pt p pt);
-                [ intro; clear HYPPD | apply HYPPD; clear HYPPD; trivial ]
-                | idtac ]
-          | _:(continuity_pt p pt) |- _ => idtac
-          |  |- (continuity_pt p pt) => idtac
-          |  |- (continuity_pt _ _) =>
-            cut (True -> continuity_pt p pt);
-              [ intro HYPPD; cut (continuity_pt p pt);
-                [ intro; clear HYPPD | apply HYPPD; clear HYPPD; trivial ]
-                | idtac ]
-          |  |- (derive_pt _ _ _ = _) =>
-            cut (True -> derivable_pt p pt);
-              [ intro HYPPD; cut (derivable_pt p pt);
-                [ intro; clear HYPPD | apply HYPPD; clear HYPPD; trivial ]
-                | idtac ]
-          | _ => idtac
-        end
-  end.
-
-(**********)
-Ltac is_diff_pt :=
-  match goal with
-    |  |- (derivable_pt Rsqr _) =>
-
-  (* fonctions de base *)
-      apply derivable_pt_Rsqr
-    |  |- (derivable_pt id ?X1) => apply (derivable_pt_id X1)
-    |  |- (derivable_pt (fct_cte _) _) => apply derivable_pt_const
-    |  |- (derivable_pt sin _) => apply derivable_pt_sin
-    |  |- (derivable_pt cos _) => apply derivable_pt_cos
-    |  |- (derivable_pt sinh _) => apply derivable_pt_sinh
-    |  |- (derivable_pt cosh _) => apply derivable_pt_cosh
-    |  |- (derivable_pt exp _) => apply derivable_pt_exp
-    |  |- (derivable_pt (pow_fct _) _) =>
-      unfold pow_fct in |- *; apply derivable_pt_pow
-    |  |- (derivable_pt sqrt ?X1) =>
-      apply (derivable_pt_sqrt X1);
-        assumption ||
-          unfold plus_fct, minus_fct, opp_fct, mult_fct, div_fct, inv_fct,
-            comp, id, fct_cte, pow_fct in |- *
-    |  |- (derivable_pt Rabs ?X1) =>
-      apply (Rderivable_pt_abs X1);
-        assumption ||
-          unfold plus_fct, minus_fct, opp_fct, mult_fct, div_fct, inv_fct,
-            comp, id, fct_cte, pow_fct in |- *
-        (* regles de differentiabilite *)
-        (* PLUS *)
-    |  |- (derivable_pt (?X1 + ?X2) ?X3) =>
-      apply (derivable_pt_plus X1 X2 X3); is_diff_pt
-       (* MOINS *)
-    |  |- (derivable_pt (?X1 - ?X2) ?X3) =>
-      apply (derivable_pt_minus X1 X2 X3); is_diff_pt
-       (* OPPOSE *)
-    |  |- (derivable_pt (- ?X1) ?X2) =>
-      apply (derivable_pt_opp X1 X2);
-        is_diff_pt
-       (* MULTIPLICATION PAR UN SCALAIRE *)
-    |  |- (derivable_pt (mult_real_fct ?X1 ?X2) ?X3) =>
-      apply (derivable_pt_scal X2 X1 X3); is_diff_pt
-       (* MULTIPLICATION *)
-    |  |- (derivable_pt (?X1 * ?X2) ?X3) =>
-      apply (derivable_pt_mult X1 X2 X3); is_diff_pt
-       (* DIVISION *)
-    |  |- (derivable_pt (?X1 / ?X2) ?X3) =>
-      apply (derivable_pt_div X1 X2 X3);
-        [ is_diff_pt
-          | is_diff_pt
-          | try
-            assumption ||
-              unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
-                comp, pow_fct, id, fct_cte in |- * ]
-    |  |- (derivable_pt (/ ?X1) ?X2) =>
-
-       (* INVERSION *)
-      apply (derivable_pt_inv X1 X2);
-        [ assumption ||
-          unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
-            comp, pow_fct, id, fct_cte in |- *
-          | is_diff_pt ]
-    |  |- (derivable_pt (comp ?X1 ?X2) ?X3) =>
-
-       (* COMPOSITION *)
-      apply (derivable_pt_comp X2 X1 X3); is_diff_pt
-    | _:(derivable_pt ?X1 ?X2) |- (derivable_pt ?X1 ?X2) =>
-      assumption
-    | _:(derivable ?X1) |- (derivable_pt ?X1 ?X2) =>
-      cut (derivable X1); [ intro HypDDPT; apply HypDDPT | assumption ]
-    |  |- (True -> derivable_pt _ _) =>
-      intro HypTruE; clear HypTruE; is_diff_pt
-    | _ =>
-      try
-        unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
-          fct_cte, comp, pow_fct in |- *
-  end.
-
-(**********)
-Ltac is_diff_glob :=
-  match goal with
-    |  |- (derivable Rsqr) =>
-  (* fonctions de base *)
-      apply derivable_Rsqr
-    |  |- (derivable id) => apply derivable_id
-    |  |- (derivable (fct_cte _)) => apply derivable_const
-    |  |- (derivable sin) => apply derivable_sin
-    |  |- (derivable cos) => apply derivable_cos
-    |  |- (derivable cosh) => apply derivable_cosh
-    |  |- (derivable sinh) => apply derivable_sinh
-    |  |- (derivable exp) => apply derivable_exp
-    |  |- (derivable (pow_fct _)) =>
-      unfold pow_fct in |- *;
-        apply derivable_pow
-        (* regles de differentiabilite *)
-        (* PLUS *)
-    |  |- (derivable (?X1 + ?X2)) =>
-      apply (derivable_plus X1 X2); is_diff_glob
-       (* MOINS *)
-    |  |- (derivable (?X1 - ?X2)) =>
-      apply (derivable_minus X1 X2); is_diff_glob
-       (* OPPOSE *)
-    |  |- (derivable (- ?X1)) =>
-      apply (derivable_opp X1);
-        is_diff_glob
-       (* MULTIPLICATION PAR UN SCALAIRE *)
-    |  |- (derivable (mult_real_fct ?X1 ?X2)) =>
-      apply (derivable_scal X2 X1); is_diff_glob
-       (* MULTIPLICATION *)
-    |  |- (derivable (?X1 * ?X2)) =>
-      apply (derivable_mult X1 X2); is_diff_glob
-       (* DIVISION *)
-    |  |- (derivable (?X1 / ?X2)) =>
-      apply (derivable_div X1 X2);
-        [ is_diff_glob
-          | is_diff_glob
-          | try
-            assumption ||
-              unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
-                id, fct_cte, comp, pow_fct in |- * ]
-    |  |- (derivable (/ ?X1)) =>
-
-       (* INVERSION *)
-      apply (derivable_inv X1);
-        [ try
-          assumption ||
-            unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
-              id, fct_cte, comp, pow_fct in |- *
-          | is_diff_glob ]
-    |  |- (derivable (comp sqrt _)) =>
-
-       (* COMPOSITION *)
-      unfold derivable in |- *; intro; try is_diff_pt
-    |  |- (derivable (comp Rabs _)) =>
-      unfold derivable in |- *; intro; try is_diff_pt
-    |  |- (derivable (comp ?X1 ?X2)) =>
-      apply (derivable_comp X2 X1); is_diff_glob
-    | _:(derivable ?X1) |- (derivable ?X1) => assumption
-    |  |- (True -> derivable _) =>
-      intro HypTruE; clear HypTruE; is_diff_glob
-    | _ =>
-      try
-        unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
-          fct_cte, comp, pow_fct in |- *
-  end.
-
-(**********)
-Ltac is_cont_pt :=
-  match goal with
-    |  |- (continuity_pt Rsqr _) =>
-
-       (* fonctions de base *)
-      apply derivable_continuous_pt; apply derivable_pt_Rsqr
-    |  |- (continuity_pt id ?X1) =>
-      apply derivable_continuous_pt; apply (derivable_pt_id X1)
-    |  |- (continuity_pt (fct_cte _) _) =>
-      apply derivable_continuous_pt; apply derivable_pt_const
-    |  |- (continuity_pt sin _) =>
-      apply derivable_continuous_pt; apply derivable_pt_sin
-    |  |- (continuity_pt cos _) =>
-      apply derivable_continuous_pt; apply derivable_pt_cos
-    |  |- (continuity_pt sinh _) =>
-      apply derivable_continuous_pt; apply derivable_pt_sinh
-    |  |- (continuity_pt cosh _) =>
-      apply derivable_continuous_pt; apply derivable_pt_cosh
-    |  |- (continuity_pt exp _) =>
-      apply derivable_continuous_pt; apply derivable_pt_exp
-    |  |- (continuity_pt (pow_fct _) _) =>
-      unfold pow_fct in |- *; apply derivable_continuous_pt;
-        apply derivable_pt_pow
-    |  |- (continuity_pt sqrt ?X1) =>
-      apply continuity_pt_sqrt;
-        assumption ||
-          unfold plus_fct, minus_fct, opp_fct, mult_fct, div_fct, inv_fct,
-            comp, id, fct_cte, pow_fct in |- *
-    |  |- (continuity_pt Rabs ?X1) =>
-      apply (Rcontinuity_abs X1)
-       (* regles de differentiabilite *)
-       (* PLUS *)
-    |  |- (continuity_pt (?X1 + ?X2) ?X3) =>
-      apply (continuity_pt_plus X1 X2 X3); is_cont_pt
-       (* MOINS *)
-    |  |- (continuity_pt (?X1 - ?X2) ?X3) =>
-      apply (continuity_pt_minus X1 X2 X3); is_cont_pt
-       (* OPPOSE *)
-    |  |- (continuity_pt (- ?X1) ?X2) =>
-      apply (continuity_pt_opp X1 X2);
-        is_cont_pt
-       (* MULTIPLICATION PAR UN SCALAIRE *)
-    |  |- (continuity_pt (mult_real_fct ?X1 ?X2) ?X3) =>
-      apply (continuity_pt_scal X2 X1 X3); is_cont_pt
-       (* MULTIPLICATION *)
-    |  |- (continuity_pt (?X1 * ?X2) ?X3) =>
-      apply (continuity_pt_mult X1 X2 X3); is_cont_pt
-       (* DIVISION *)
-    |  |- (continuity_pt (?X1 / ?X2) ?X3) =>
-      apply (continuity_pt_div X1 X2 X3);
-        [ is_cont_pt
-          | is_cont_pt
-          | try
-            assumption ||
-              unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
-                comp, id, fct_cte, pow_fct in |- * ]
-    |  |- (continuity_pt (/ ?X1) ?X2) =>
-
-       (* INVERSION *)
-      apply (continuity_pt_inv X1 X2);
-        [ is_cont_pt
-          | assumption ||
-            unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
-              comp, id, fct_cte, pow_fct in |- * ]
-    |  |- (continuity_pt (comp ?X1 ?X2) ?X3) =>
-
-       (* COMPOSITION *)
-      apply (continuity_pt_comp X2 X1 X3); is_cont_pt
-    | _:(continuity_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) =>
-      assumption
-    | _:(continuity ?X1) |- (continuity_pt ?X1 ?X2) =>
-      cut (continuity X1); [ intro HypDDPT; apply HypDDPT | assumption ]
-    | _:(derivable_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) =>
-      apply derivable_continuous_pt; assumption
-    | _:(derivable ?X1) |- (continuity_pt ?X1 ?X2) =>
-      cut (continuity X1);
-        [ intro HypDDPT; apply HypDDPT
-          | apply derivable_continuous; assumption ]
-    |  |- (True -> continuity_pt _ _) =>
-      intro HypTruE; clear HypTruE; is_cont_pt
-    | _ =>
-      try
-        unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
-          fct_cte, comp, pow_fct in |- *
-  end.
-
-(**********)
-Ltac is_cont_glob :=
-  match goal with
-    |  |- (continuity Rsqr) =>
-
-       (* fonctions de base *)
-      apply derivable_continuous; apply derivable_Rsqr
-    |  |- (continuity id) => apply derivable_continuous; apply derivable_id
-    |  |- (continuity (fct_cte _)) =>
-      apply derivable_continuous; apply derivable_const
-    |  |- (continuity sin) => apply derivable_continuous; apply derivable_sin
-    |  |- (continuity cos) => apply derivable_continuous; apply derivable_cos
-    |  |- (continuity exp) => apply derivable_continuous; apply derivable_exp
-    |  |- (continuity (pow_fct _)) =>
-      unfold pow_fct in |- *; apply derivable_continuous; apply derivable_pow
-    |  |- (continuity sinh) =>
-      apply derivable_continuous; apply derivable_sinh
-    |  |- (continuity cosh) =>
-      apply derivable_continuous; apply derivable_cosh
-    |  |- (continuity Rabs) =>
-      apply Rcontinuity_abs
-       (* regles de continuite *)
-       (* PLUS *)
-    |  |- (continuity (?X1 + ?X2)) =>
-      apply (continuity_plus X1 X2);
-        try is_cont_glob || assumption
-            (* MOINS *)
-    |  |- (continuity (?X1 - ?X2)) =>
-      apply (continuity_minus X1 X2);
-        try is_cont_glob || assumption
-            (* OPPOSE *)
-    |  |- (continuity (- ?X1)) =>
-      apply (continuity_opp X1); try is_cont_glob || assumption
-                                      (* INVERSE *)
-    |  |- (continuity (/ ?X1)) =>
-      apply (continuity_inv X1);
-        try is_cont_glob || assumption
-            (* MULTIPLICATION PAR UN SCALAIRE *)
-    |  |- (continuity (mult_real_fct ?X1 ?X2)) =>
-      apply (continuity_scal X2 X1);
-        try is_cont_glob || assumption
-            (* MULTIPLICATION *)
-    |  |- (continuity (?X1 * ?X2)) =>
-      apply (continuity_mult X1 X2);
-        try is_cont_glob || assumption
-            (* DIVISION *)
-    |  |- (continuity (?X1 / ?X2)) =>
-      apply (continuity_div X1 X2);
-        [ try is_cont_glob || assumption
-          | try is_cont_glob || assumption
-          | try
-            assumption ||
-              unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
-                id, fct_cte, pow_fct in |- * ]
-    |  |- (continuity (comp sqrt _)) =>
-
-       (* COMPOSITION *)
-      unfold continuity_pt in |- *; intro; try is_cont_pt
-    |  |- (continuity (comp ?X1 ?X2)) =>
-      apply (continuity_comp X2 X1); try is_cont_glob || assumption
-    | _:(continuity ?X1) |- (continuity ?X1) => assumption
-    |  |- (True -> continuity _) =>
-      intro HypTruE; clear HypTruE; is_cont_glob
-    | _:(derivable ?X1) |- (continuity ?X1) =>
-      apply derivable_continuous; assumption
-    | _ =>
-      try
-        unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
-          fct_cte, comp, pow_fct in |- *
-  end.
-
-(**********)
-Ltac rew_term trm :=
-  match constr:trm with
-    | (?X1 + ?X2) =>
-      let p1 := rew_term X1 with p2 := rew_term X2 in
-        match constr:p1 with
-          | (fct_cte ?X3) =>
-            match constr:p2 with
-              | (fct_cte ?X4) => constr:(fct_cte (X3 + X4))
-              | _ => constr:(p1 + p2)%F
-            end
-          | _ => constr:(p1 + p2)%F
-        end
-    | (?X1 - ?X2) =>
-      let p1 := rew_term X1 with p2 := rew_term X2 in
-        match constr:p1 with
-          | (fct_cte ?X3) =>
-            match constr:p2 with
-              | (fct_cte ?X4) => constr:(fct_cte (X3 - X4))
-              | _ => constr:(p1 - p2)%F
-            end
-          | _ => constr:(p1 - p2)%F
-        end
-    | (?X1 / ?X2) =>
-      let p1 := rew_term X1 with p2 := rew_term X2 in
-        match constr:p1 with
-          | (fct_cte ?X3) =>
-            match constr:p2 with
-              | (fct_cte ?X4) => constr:(fct_cte (X3 / X4))
-              | _ => constr:(p1 / p2)%F
-            end
-          | _ =>
-            match constr:p2 with
-              | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F
-              | _ => constr:(p1 / p2)%F
-            end
-        end
-    | (?X1 * / ?X2) =>
-      let p1 := rew_term X1 with p2 := rew_term X2 in
-        match constr:p1 with
-          | (fct_cte ?X3) =>
-            match constr:p2 with
-              | (fct_cte ?X4) => constr:(fct_cte (X3 / X4))
-              | _ => constr:(p1 / p2)%F
-            end
-          | _ =>
-            match constr:p2 with
-              | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F
-              | _ => constr:(p1 / p2)%F
-            end
-        end
-    | (?X1 * ?X2) =>
-      let p1 := rew_term X1 with p2 := rew_term X2 in
-        match constr:p1 with
-          | (fct_cte ?X3) =>
-            match constr:p2 with
-              | (fct_cte ?X4) => constr:(fct_cte (X3 * X4))
-              | _ => constr:(p1 * p2)%F
-            end
-          | _ => constr:(p1 * p2)%F
-        end
-    | (- ?X1) =>
-      let p := rew_term X1 in
-        match constr:p with
-          | (fct_cte ?X2) => constr:(fct_cte (- X2))
-          | _ => constr:(- p)%F
-        end
-    | (/ ?X1) =>
-      let p := rew_term X1 in
-        match constr:p with
-          | (fct_cte ?X2) => constr:(fct_cte (/ X2))
-          | _ => constr:(/ p)%F
-        end
-    | (?X1 AppVar) => constr:X1
-    | (?X1 ?X2) =>
-      let p := rew_term X2 in
-        match constr:p with
-          | (fct_cte ?X3) => constr:(fct_cte (X1 X3))
-          | _ => constr:(comp X1 p)
-        end
-    | AppVar => constr:id
-    | (AppVar ^ ?X1) => constr:(pow_fct X1)
-    | (?X1 ^ ?X2) =>
-      let p := rew_term X1 in
-        match constr:p with
-          | (fct_cte ?X3) => constr:(fct_cte (pow_fct X2 X3))
-          | _ => constr:(comp (pow_fct X2) p)
-        end
-    | ?X1 => constr:(fct_cte X1)
-  end.
-
-(**********)
-Ltac deriv_proof trm pt :=
-  match constr:trm with
-    | (?X1 + ?X2)%F =>
-      let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
-        constr:(derivable_pt_plus X1 X2 pt p1 p2)
-    | (?X1 - ?X2)%F =>
-      let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
-        constr:(derivable_pt_minus X1 X2 pt p1 p2)
-    | (?X1 * ?X2)%F =>
-      let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
-        constr:(derivable_pt_mult X1 X2 pt p1 p2)
-    | (?X1 / ?X2)%F =>
-      match goal with
-        | id:(?X2 pt <> 0) |- _ =>
-          let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
-            constr:(derivable_pt_div X1 X2 pt p1 p2 id)
-        | _ => constr:False
-      end
-    | (/ ?X1)%F =>
-      match goal with
-        | id:(?X1 pt <> 0) |- _ =>
-          let p1 := deriv_proof X1 pt in
-            constr:(derivable_pt_inv X1 pt p1 id)
-        | _ => constr:False
-      end
-    | (comp ?X1 ?X2) =>
-      let pt_f1 := eval cbv beta in (X2 pt) in
-        let p1 := deriv_proof X1 pt_f1 with p2 := deriv_proof X2 pt in
-          constr:(derivable_pt_comp X2 X1 pt p2 p1)
-    | (- ?X1)%F =>
-      let p1 := deriv_proof X1 pt in
-        constr:(derivable_pt_opp X1 pt p1)
-    | sin => constr:(derivable_pt_sin pt)
-    | cos => constr:(derivable_pt_cos pt)
-    | sinh => constr:(derivable_pt_sinh pt)
-    | cosh => constr:(derivable_pt_cosh pt)
-    | exp => constr:(derivable_pt_exp pt)
-    | id => constr:(derivable_pt_id pt)
-    | Rsqr => constr:(derivable_pt_Rsqr pt)
-    | sqrt =>
-      match goal with
-        | id:(0 < pt) |- _ => constr:(derivable_pt_sqrt pt id)
-        | _ => constr:False
-      end
-    | (fct_cte ?X1) => constr:(derivable_pt_const X1 pt)
-    | ?X1 =>
-      let aux := constr:X1 in
-        match goal with
-          | id:(derivable_pt aux pt) |- _ => constr:id
-          | id:(derivable aux) |- _ => constr:(id pt)
-          | _ => constr:False
-        end
-  end.
-
-(**********)
-Ltac simplify_derive trm pt :=
-  match constr:trm with
-    | (?X1 + ?X2)%F =>
-      try rewrite derive_pt_plus; simplify_derive X1 pt;
-        simplify_derive X2 pt
-    | (?X1 - ?X2)%F =>
-      try rewrite derive_pt_minus; simplify_derive X1 pt;
-        simplify_derive X2 pt
-    | (?X1 * ?X2)%F =>
-      try rewrite derive_pt_mult; simplify_derive X1 pt;
-        simplify_derive X2 pt
-    | (?X1 / ?X2)%F =>
-      try rewrite derive_pt_div; simplify_derive X1 pt; simplify_derive X2 pt
-    | (comp ?X1 ?X2) =>
-      let pt_f1 := eval cbv beta in (X2 pt) in
-        (try rewrite derive_pt_comp; simplify_derive X1 pt_f1;
-          simplify_derive X2 pt)
-    | (- ?X1)%F => try rewrite derive_pt_opp; simplify_derive X1 pt
-    | (/ ?X1)%F =>
-      try rewrite derive_pt_inv; simplify_derive X1 pt
-    | (fct_cte ?X1) => try rewrite derive_pt_const
-    | id => try rewrite derive_pt_id
-    | sin => try rewrite derive_pt_sin
-    | cos => try rewrite derive_pt_cos
-    | sinh => try rewrite derive_pt_sinh
-    | cosh => try rewrite derive_pt_cosh
-    | exp => try rewrite derive_pt_exp
-    | Rsqr => try rewrite derive_pt_Rsqr
-    | sqrt => try rewrite derive_pt_sqrt
-    | ?X1 =>
-      let aux := constr:X1 in
-        match goal with
-          | id:(derive_pt aux pt ?X2 = _),H:(derivable aux) |- _ =>
-            try replace (derive_pt aux pt (H pt)) with (derive_pt aux pt X2);
-              [ rewrite id | apply pr_nu ]
-          | id:(derive_pt aux pt ?X2 = _),H:(derivable_pt aux pt) |- _ =>
-            try replace (derive_pt aux pt H) with (derive_pt aux pt X2);
-              [ rewrite id | apply pr_nu ]
-          | _ => idtac
-        end
-    | _ => idtac
-  end.
-
-(**********)
-Ltac reg :=
-  match goal with
-    |  |- (derivable_pt ?X1 ?X2) =>
-      let trm := eval cbv beta in (X1 AppVar) in
-        let aux := rew_term trm in
-          (intro_hyp_pt aux X2;
-            try (change (derivable_pt aux X2) in |- *; is_diff_pt) || is_diff_pt)
-    |  |- (derivable ?X1) =>
-      let trm := eval cbv beta in (X1 AppVar) in
-        let aux := rew_term trm in
-          (intro_hyp_glob aux;
-            try (change (derivable aux) in |- *; is_diff_glob) || is_diff_glob)
-    |  |- (continuity ?X1) =>
-      let trm := eval cbv beta in (X1 AppVar) in
-        let aux := rew_term trm in
-          (intro_hyp_glob aux;
-            try (change (continuity aux) in |- *; is_cont_glob) || is_cont_glob)
-    |  |- (continuity_pt ?X1 ?X2) =>
-      let trm := eval cbv beta in (X1 AppVar) in
-        let aux := rew_term trm in
-          (intro_hyp_pt aux X2;
-            try (change (continuity_pt aux X2) in |- *; is_cont_pt) || is_cont_pt)
-    |  |- (derive_pt ?X1 ?X2 ?X3 = ?X4) =>
-      let trm := eval cbv beta in (X1 AppVar) in
-      let aux := rew_term trm in
-      intro_hyp_pt aux X2;
-      (let aux2 := deriv_proof aux X2 in
-       try
-         (replace (derive_pt X1 X2 X3) with (derive_pt aux X2 aux2);
-           [ simplify_derive aux X2;
-             try unfold plus_fct, minus_fct, mult_fct, div_fct, id, fct_cte,
-                        inv_fct, opp_fct in |- *; ring || ring_simplify
-           | try apply pr_nu ]) || is_diff_pt)
-  end.
+Require Export Ranalysis_reg.
\ No newline at end of file