These files are displaced from Rtrigo.v and Ranalysis_reg.v

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

2 files changed, 2869 insertions, 0 deletions

diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v
new file mode 100644
index 000000000..2026dd82e
--- /dev/null
+++ b/theories/Reals/Ranalysis_reg.v
@@ -0,0 +1,800 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Rbase.
+Require Import Rfunctions.
+Require Import Rtrigo1.
+Require Import SeqSeries.
+Require Export Ranalysis1.
+Require Export Ranalysis2.
+Require Export Ranalysis3.
+Require Export Rtopology.
+Require Export MVT.
+Require Export PSeries_reg.
+Require Export Exp_prop.
+Require Export Rtrigo_reg.
+Require Export Rsqrt_def.
+Require Export R_sqrt.
+Require Export Rtrigo_calc.
+Require Export Rgeom.
+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.
diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v
new file mode 100644
index 000000000..88bf0e084
--- /dev/null
+++ b/theories/Reals/Rtrigo1.v
@@ -0,0 +1,2069 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Rbase.
+Require Import Rfunctions.
+Require Import SeqSeries.
+Require Export Rtrigo_fun.
+Require Export Rtrigo_def.
+Require Export Rtrigo_alt.
+Require Export Cos_rel.
+Require Export Cos_plus.
+Require Import ZArith_base.
+Require Import Zcomplements.
+Require Import Classical_Prop.
+Require Import Fourier.
+Require Import Ranalysis1.
+Require Import Rsqrt_def. 
+Require Import PSeries_reg.
+
+Local Open Scope nat_scope.
+Local Open Scope R_scope.
+
+Lemma CVN_R_cos :
+  forall fn:nat -> R -> R,
+    fn = (fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)) ->
+    CVN_R fn.
+Proof.
+  unfold CVN_R in |- *; intros.
+  cut ((r:R) <> 0).
+  intro hyp_r; unfold CVN_r in |- *.
+  exists (fun n:nat => / INR (fact (2 * n)) * r ^ (2 * n)).
+  cut
+    { l:R |
+        Un_cv
+        (fun n:nat =>
+          sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k)) * r ^ (2 * k)))
+          n) l }.
+  intro X; elim X; intros.
+  exists x.
+  split.
+  apply p.
+  intros; rewrite H; unfold Rdiv in |- *; do 2 rewrite Rabs_mult.
+  rewrite pow_1_abs; rewrite Rmult_1_l.
+  cut (0 < / INR (fact (2 * n))).
+  intro; rewrite (Rabs_right _ (Rle_ge _ _ (Rlt_le _ _ H1))).
+  apply Rmult_le_compat_l.
+  left; apply H1.
+  rewrite <- RPow_abs; apply pow_maj_Rabs.
+  rewrite Rabs_Rabsolu.
+  unfold Boule in H0; rewrite Rminus_0_r in H0.
+  left; apply H0.
+  apply Rinv_0_lt_compat; apply INR_fact_lt_0.
+  apply Alembert_C2.
+  intro; apply Rabs_no_R0.
+  apply prod_neq_R0.
+  apply Rinv_neq_0_compat.
+  apply INR_fact_neq_0.
+  apply pow_nonzero; assumption.
+  assert (H0 := Alembert_cos).
+  unfold cos_n in H0; unfold Un_cv in H0; unfold Un_cv in |- *; intros.
+  cut (0 < eps / Rsqr r).
+  intro; elim (H0 _ H2); intros N0 H3.
+  exists N0; intros.
+  unfold R_dist in |- *; assert (H5 := H3 _ H4).
+  unfold R_dist in H5;
+    replace
+    (Rabs
+      (Rabs (/ INR (fact (2 * S n)) * r ^ (2 * S n)) /
+        Rabs (/ INR (fact (2 * n)) * r ^ (2 * n)))) with
+    (Rsqr r *
+      Rabs ((-1) ^ S n / INR (fact (2 * S n)) / ((-1) ^ n / INR (fact (2 * n))))).
+  apply Rmult_lt_reg_l with (/ Rsqr r).
+  apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption.
+  pattern (/ Rsqr r) at 1 in |- *; replace (/ Rsqr r) with (Rabs (/ Rsqr r)).
+  rewrite <- Rabs_mult; rewrite Rmult_minus_distr_l; rewrite Rmult_0_r;
+    rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_l; rewrite <- (Rmult_comm eps); apply H5.
+  unfold Rsqr in |- *; apply prod_neq_R0; assumption.
+  rewrite Rabs_Rinv.
+  rewrite Rabs_right.
+  reflexivity.
+  apply Rle_ge; apply Rle_0_sqr.
+  unfold Rsqr in |- *; apply prod_neq_R0; assumption.
+  rewrite (Rmult_comm (Rsqr r)); unfold Rdiv in |- *; repeat rewrite Rabs_mult;
+    rewrite Rabs_Rabsolu; rewrite pow_1_abs; rewrite Rmult_1_l;
+      repeat rewrite Rmult_assoc; apply Rmult_eq_compat_l.
+  rewrite Rabs_Rinv.
+  rewrite Rabs_mult; rewrite (pow_1_abs n); rewrite Rmult_1_l;
+    rewrite <- Rabs_Rinv.
+  rewrite Rinv_involutive.
+  rewrite Rinv_mult_distr.
+  rewrite Rabs_Rinv.
+  rewrite Rinv_involutive.
+  rewrite (Rmult_comm (Rabs (Rabs (r ^ (2 * S n))))); rewrite Rabs_mult;
+    rewrite Rabs_Rabsolu; rewrite Rmult_assoc; apply Rmult_eq_compat_l.
+  rewrite Rabs_Rinv.
+  do 2 rewrite Rabs_Rabsolu; repeat rewrite Rabs_right.
+  replace (r ^ (2 * S n)) with (r ^ (2 * n) * r * r).
+  repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
+  unfold Rsqr in |- *; ring.
+  apply pow_nonzero; assumption.
+  replace (2 * S n)%nat with (S (S (2 * n))).
+  simpl in |- *; ring.
+  ring.
+  apply Rle_ge; apply pow_le; left; apply (cond_pos r).
+  apply Rle_ge; apply pow_le; left; apply (cond_pos r).
+  apply Rabs_no_R0; apply pow_nonzero; assumption.
+  apply Rabs_no_R0; apply INR_fact_neq_0.
+  apply INR_fact_neq_0.
+  apply Rabs_no_R0; apply Rinv_neq_0_compat; apply INR_fact_neq_0.
+  apply Rabs_no_R0; apply pow_nonzero; assumption.
+  apply INR_fact_neq_0.
+  apply Rinv_neq_0_compat; apply INR_fact_neq_0.
+  apply prod_neq_R0.
+  apply pow_nonzero; discrR.
+  apply Rinv_neq_0_compat; apply INR_fact_neq_0.
+  unfold Rdiv in |- *; apply Rmult_lt_0_compat.
+  apply H1.
+  apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption.
+  assert (H0 := cond_pos r); red in |- *; intro; rewrite H1 in H0;
+    elim (Rlt_irrefl _ H0).
+Qed.
+
+(**********)
+Lemma continuity_cos : continuity cos.
+Proof.
+  set (fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)).
+  cut (CVN_R fn).
+  intro; cut (forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }).
+  intro cv; cut (forall n:nat, continuity (fn n)).
+  intro; cut (forall x:R, cos x = SFL fn cv x).
+  intro; cut (continuity (SFL fn cv) -> continuity cos).
+  intro; apply H1.
+  apply SFL_continuity; assumption.
+  unfold continuity in |- *; unfold continuity_pt in |- *;
+    unfold continue_in in |- *; unfold limit1_in in |- *;
+      unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *;
+        intros.
+  elim (H1 x _ H2); intros.
+  exists x0; intros.
+  elim H3; intros.
+  split.
+  apply H4.
+  intros; rewrite (H0 x); rewrite (H0 x1); apply H5; apply H6.
+  intro; unfold cos, SFL in |- *.
+  case (cv x); case (exist_cos (Rsqr x)); intros.
+  symmetry  in |- *; eapply UL_sequence.
+  apply u.
+  unfold cos_in in c; unfold infinite_sum in c; unfold Un_cv in |- *; intros.
+  elim (c _ H0); intros N0 H1.
+  exists N0; intros.
+  unfold R_dist in H1; unfold R_dist, SP in |- *.
+  replace (sum_f_R0 (fun k:nat => fn k x) n) with
+  (sum_f_R0 (fun i:nat => cos_n i * Rsqr x ^ i) n).
+  apply H1; assumption.
+  apply sum_eq; intros.
+  unfold cos_n, fn in |- *; apply Rmult_eq_compat_l.
+  unfold Rsqr in |- *; rewrite pow_sqr; reflexivity.
+  intro; unfold fn in |- *;
+    replace (fun x:R => (-1) ^ n / INR (fact (2 * n)) * x ^ (2 * n)) with
+    (fct_cte ((-1) ^ n / INR (fact (2 * n))) * pow_fct (2 * n))%F;
+    [ idtac | reflexivity ].
+  apply continuity_mult.
+  apply derivable_continuous; apply derivable_const.
+  apply derivable_continuous; apply (derivable_pow (2 * n)).
+  apply CVN_R_CVS; apply X.
+  apply CVN_R_cos; unfold fn in |- *; reflexivity.
+Qed.
+
+Lemma sin_gt_cos_7_8 : sin (7 / 8) > cos (7 / 8).
+Proof. 
+assert (lo1 : 0 <= 7/8) by fourier.
+assert (up1 : 7/8 <= 4) by fourier.
+assert (lo : -2 <= 7/8) by fourier.
+assert (up : 7/8 <= 2) by fourier.
+destruct (pre_sin_bound _ 0 lo1 up1) as [lower _ ].
+destruct (pre_cos_bound _ 0 lo up) as [_ upper].
+apply Rle_lt_trans with (1 := upper).
+apply Rlt_le_trans with (2 := lower).
+unfold cos_approx, sin_approx.
+simpl sum_f_R0; replace 7 with (IZR 7) by (simpl; field).
+replace 8 with (IZR 8) by (simpl; field).
+unfold cos_term, sin_term; simpl fact; rewrite !INR_IZR_INZ.
+simpl plus; simpl mult.
+field_simplify;
+  try (repeat apply conj; apply not_eq_sym, Rlt_not_eq, (IZR_lt 0); reflexivity).
+unfold Rminus; rewrite !pow_IZR, <- !mult_IZR, <- !opp_IZR, <- ?plus_IZR.
+match goal with 
+  |- IZR ?a / ?b < ?c / ?d =>
+  apply Rmult_lt_reg_r with d;[apply (IZR_lt 0); reflexivity |
+    unfold Rdiv at 2; rewrite Rmult_assoc, Rinv_l, Rmult_1_r, Rmult_comm;
+     [ |apply not_eq_sym, Rlt_not_eq, (IZR_lt 0); reflexivity ]];
+  apply Rmult_lt_reg_r with b;[apply (IZR_lt 0); reflexivity | ]
+end.
+unfold Rdiv; rewrite !Rmult_assoc, Rinv_l, Rmult_1_r;
+ [ | apply not_eq_sym, Rlt_not_eq, (IZR_lt 0); reflexivity].
+repeat (rewrite <- !plus_IZR || rewrite <- !mult_IZR).
+apply IZR_lt; reflexivity.
+Qed.
+
+Definition PI_2_aux : {z | 7/8 <= z <= 7/4 /\ -cos z = 0}.
+assert (cc : continuity (fun r =>- cos r)).
+ apply continuity_opp, continuity_cos.
+assert (cvp : 0 < cos (7/8)).
+ assert (int78 : -2 <= 7/8 <= 2) by (split; fourier).
+ destruct int78 as [lower upper].
+ case (pre_cos_bound _ 0 lower upper).
+ unfold cos_approx; simpl sum_f_R0; unfold cos_term.
+ intros cl _; apply Rlt_le_trans with (2 := cl); simpl.
+ fourier.
+assert (cun : cos (7/4) < 0).
+ replace (7/4) with (7/8 + 7/8) by field.
+ rewrite cos_plus.
+ apply Rlt_minus; apply Rsqr_incrst_1.
+   exact sin_gt_cos_7_8.
+  apply Rlt_le; assumption.
+ apply Rlt_le; apply Rlt_trans with (1 := cvp); exact sin_gt_cos_7_8.
+apply IVT; auto; fourier.
+Qed.
+
+Definition PI2 := proj1_sig PI_2_aux.
+
+Definition PI := 2 * PI2.
+
+Lemma cos_pi2 : cos PI2 = 0.
+unfold PI2; case PI_2_aux; simpl.
+intros x [_ q]; rewrite <- (Ropp_involutive (cos x)), q; apply Ropp_0.
+Qed.
+
+Lemma pi2_int : 7/8 <= PI2 <= 7/4.
+unfold PI2; case PI_2_aux; simpl; tauto.
+Qed.
+
+(**********)
+Lemma cos_minus : forall x y:R, cos (x - y) = cos x * cos y + sin x * sin y.
+Proof.
+  intros; unfold Rminus in |- *; rewrite cos_plus.
+  rewrite <- cos_sym; rewrite sin_antisym; ring.
+Qed.
+
+(**********)
+Lemma sin2_cos2 : forall x:R, Rsqr (sin x) + Rsqr (cos x) = 1.
+Proof.
+  intro; unfold Rsqr in |- *; rewrite Rplus_comm; rewrite <- (cos_minus x x);
+    unfold Rminus in |- *; rewrite Rplus_opp_r; apply cos_0.
+Qed.
+
+Lemma cos2 : forall x:R, Rsqr (cos x) = 1 - Rsqr (sin x).
+Proof.
+  intros x; rewrite <- (sin2_cos2 x); ring.
+Qed.
+
+Lemma sin2 : forall x:R, Rsqr (sin x) = 1 - Rsqr (cos x).
+Proof.
+  intro x; generalize (cos2 x); intro H1; rewrite H1.
+  unfold Rminus in |- *; rewrite Ropp_plus_distr; rewrite <- Rplus_assoc;
+    rewrite Rplus_opp_r; rewrite Rplus_0_l; symmetry  in |- *;
+      apply Ropp_involutive.
+Qed.
+
+(**********)
+Lemma cos_PI2 : cos (PI / 2) = 0.
+Proof.
+ unfold PI; generalize cos_pi2; replace ((2 * PI2)/2) with PI2 by field; tauto.
+Qed.
+
+Lemma sin_pos_tech : forall x, 0 < x < 2 -> 0 < sin x. 
+intros x [int1 int2].
+assert (lo : 0 <= x) by (apply Rlt_le; assumption).
+assert (up : x <= 4) by (apply Rlt_le, Rlt_trans with (1:=int2); fourier).
+destruct (pre_sin_bound _ 0 lo up) as [t _]; clear lo up.
+apply Rlt_le_trans with (2:= t); clear t.
+unfold sin_approx; simpl sum_f_R0; unfold sin_term; simpl.
+match goal with |- _ < ?a =>
+  replace a with (x * (1 - x^2/6)) by (simpl; field)
+end.
+assert (t' : x ^ 2 <= 4).
+ replace 4 with (2 ^ 2) by field.
+ apply (pow_incr x 2); split; apply Rlt_le; assumption.
+apply Rmult_lt_0_compat;[assumption | fourier ].
+Qed.
+
+Lemma sin_PI2 : sin (PI / 2) = 1.
+replace (PI / 2) with PI2 by (unfold PI; field).
+assert (int' : 0 < PI2 < 2).
+ destruct pi2_int; split; fourier.
+assert (lo2 := sin_pos_tech PI2 int').
+assert (t2 : Rabs (sin PI2) = 1).
+ rewrite <- Rabs_R1; apply Rsqr_eq_abs_0.
+ rewrite Rsqr_1, sin2, cos_pi2, Rsqr_0, Rminus_0_r; reflexivity.
+revert t2; rewrite Rabs_pos_eq;[| apply Rlt_le]; tauto.
+Qed.
+
+Lemma PI_RGT_0 : PI > 0.
+Proof. unfold PI; destruct pi2_int; fourier. Qed.
+
+Lemma PI_4 : PI <= 4.
+Proof. unfold PI; destruct pi2_int; fourier. Qed.
+
+(**********)
+Lemma PI_neq0 : PI <> 0.
+Proof.
+  red in |- *; intro; assert (H0 := PI_RGT_0); rewrite H in H0;
+    elim (Rlt_irrefl _ H0).
+Qed.
+
+
+(**********)
+Lemma cos_PI : cos PI = -1.
+Proof.
+  replace PI with (PI / 2 + PI / 2).
+  rewrite cos_plus.
+  rewrite sin_PI2; rewrite cos_PI2.
+  ring.
+  symmetry  in |- *; apply double_var.
+Qed.
+
+Lemma sin_PI : sin PI = 0.
+Proof.
+  assert (H := sin2_cos2 PI).
+  rewrite cos_PI in H.
+  rewrite <- Rsqr_neg in H.
+  rewrite Rsqr_1 in H.
+  cut (Rsqr (sin PI) = 0).
+  intro; apply (Rsqr_eq_0 _ H0).
+  apply Rplus_eq_reg_l with 1.
+  rewrite Rplus_0_r; rewrite Rplus_comm; exact H.
+Qed.
+
+Lemma sin_bound : forall (a : R) (n : nat), 0 <= a -> a <= PI ->
+       sin_approx a (2 * n + 1) <= sin a <= sin_approx a (2 * (n + 1)).
+Proof.
+intros a n a0 api; apply pre_sin_bound.
+ assumption.
+apply Rle_trans with (1:= api) (2 := PI_4).
+Qed.
+
+Lemma cos_bound : forall (a : R) (n : nat), - PI / 2 <= a -> a <= PI / 2 ->
+       cos_approx a (2 * n + 1) <= cos a <= cos_approx a (2 * (n + 1)).
+Proof.
+intros a n lower upper; apply pre_cos_bound.
+ apply Rle_trans with (2 := lower).
+ apply Rmult_le_reg_r with 2; [fourier |].
+ replace ((-PI/2) * 2) with (-PI) by field.
+ assert (t := PI_4); fourier.
+apply Rle_trans with (1 := upper).
+apply Rmult_le_reg_r with 2; [fourier | ].
+replace ((PI/2) * 2) with PI by field.
+generalize PI_4; intros; fourier.
+Qed.
+(**********)
+Lemma neg_cos : forall x:R, cos (x + PI) = - cos x.
+Proof.
+  intro x; rewrite cos_plus; rewrite sin_PI; rewrite cos_PI; ring.
+Qed.
+
+(**********)
+Lemma sin_cos : forall x:R, sin x = - cos (PI / 2 + x).
+Proof.
+  intro x; rewrite cos_plus; rewrite sin_PI2; rewrite cos_PI2; ring.
+Qed.
+
+(**********)
+Lemma sin_plus : forall x y:R, sin (x + y) = sin x * cos y + cos x * sin y.
+Proof.
+  intros.
+  rewrite (sin_cos (x + y)).
+  replace (PI / 2 + (x + y)) with (PI / 2 + x + y); [ rewrite cos_plus | ring ].
+  rewrite (sin_cos (PI / 2 + x)).
+  replace (PI / 2 + (PI / 2 + x)) with (x + PI).
+  rewrite neg_cos.
+  replace (cos (PI / 2 + x)) with (- sin x).
+  ring.
+  rewrite sin_cos; rewrite Ropp_involutive; reflexivity.
+  pattern PI at 1 in |- *; rewrite (double_var PI); ring.
+Qed.
+
+Lemma sin_minus : forall x y:R, sin (x - y) = sin x * cos y - cos x * sin y.
+Proof.
+  intros; unfold Rminus in |- *; rewrite sin_plus.
+  rewrite <- cos_sym; rewrite sin_antisym; ring.
+Qed.
+
+(**********)
+Definition tan (x:R) : R := sin x / cos x.
+
+Lemma tan_plus :
+  forall x y:R,
+    cos x <> 0 ->
+    cos y <> 0 ->
+    cos (x + y) <> 0 ->
+    1 - tan x * tan y <> 0 ->
+    tan (x + y) = (tan x + tan y) / (1 - tan x * tan y).
+Proof.
+  intros; unfold tan in |- *; rewrite sin_plus; rewrite cos_plus;
+    unfold Rdiv in |- *;
+      replace (cos x * cos y - sin x * sin y) with
+      (cos x * cos y * (1 - sin x * / cos x * (sin y * / cos y))).
+  rewrite Rinv_mult_distr.
+  repeat rewrite <- Rmult_assoc;
+    replace ((sin x * cos y + cos x * sin y) * / (cos x * cos y)) with
+    (sin x * / cos x + sin y * / cos y).
+  reflexivity.
+  rewrite Rmult_plus_distr_r; rewrite Rinv_mult_distr.
+  repeat rewrite Rmult_assoc; repeat rewrite (Rmult_comm (sin x));
+    repeat rewrite <- Rmult_assoc.
+  repeat rewrite Rinv_r_simpl_m; [ reflexivity | assumption | assumption ].
+  assumption.
+  assumption.
+  apply prod_neq_R0; assumption.
+  assumption.
+  unfold Rminus in |- *; rewrite Rmult_plus_distr_l; rewrite Rmult_1_r;
+    apply Rplus_eq_compat_l; repeat rewrite Rmult_assoc;
+      rewrite (Rmult_comm (sin x)); rewrite (Rmult_comm (cos y));
+        rewrite <- Ropp_mult_distr_r_reverse; repeat rewrite <- Rmult_assoc;
+          rewrite <- Rinv_r_sym.
+  rewrite Rmult_1_l; rewrite (Rmult_comm (sin x));
+    rewrite <- Ropp_mult_distr_r_reverse; repeat rewrite Rmult_assoc;
+      apply Rmult_eq_compat_l; rewrite (Rmult_comm (/ cos y));
+        rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
+  apply Rmult_1_r.
+  assumption.
+  assumption.
+Qed.
+
+(*******************************************************)
+(** * Some properties of cos, sin and tan              *)
+(*******************************************************)
+
+Lemma sin_2a : forall x:R, sin (2 * x) = 2 * sin x * cos x.
+Proof.
+  intro x; rewrite double; rewrite sin_plus.
+  rewrite <- (Rmult_comm (sin x)); symmetry  in |- *; rewrite Rmult_assoc;
+    apply double.
+Qed.
+
+Lemma cos_2a : forall x:R, cos (2 * x) = cos x * cos x - sin x * sin x.
+Proof.
+  intro x; rewrite double; apply cos_plus.
+Qed.
+
+Lemma cos_2a_cos : forall x:R, cos (2 * x) = 2 * cos x * cos x - 1.
+Proof.
+  intro x; rewrite double; unfold Rminus in |- *; rewrite Rmult_assoc;
+    rewrite cos_plus; generalize (sin2_cos2 x); rewrite double;
+      intro H1; rewrite <- H1; ring_Rsqr.
+Qed.
+
+Lemma cos_2a_sin : forall x:R, cos (2 * x) = 1 - 2 * sin x * sin x.
+Proof.
+  intro x; rewrite Rmult_assoc; unfold Rminus in |- *; repeat rewrite double.
+  generalize (sin2_cos2 x); intro H1; rewrite <- H1; rewrite cos_plus;
+    ring_Rsqr.
+Qed.
+
+Lemma tan_2a :
+  forall x:R,
+    cos x <> 0 ->
+    cos (2 * x) <> 0 ->
+    1 - tan x * tan x <> 0 -> tan (2 * x) = 2 * tan x / (1 - tan x * tan x).
+Proof.
+  repeat rewrite double; intros; repeat rewrite double; rewrite double in H0;
+    apply tan_plus; assumption.
+Qed.
+
+Lemma sin_neg : forall x:R, sin (- x) = - sin x.
+Proof.
+  apply sin_antisym.
+Qed.
+
+Lemma cos_neg : forall x:R, cos (- x) = cos x.
+Proof.
+  intro; symmetry  in |- *; apply cos_sym.
+Qed.
+
+Lemma tan_0 : tan 0 = 0.
+Proof.
+  unfold tan in |- *; rewrite sin_0; rewrite cos_0.
+  unfold Rdiv in |- *; apply Rmult_0_l.
+Qed.
+
+Lemma tan_neg : forall x:R, tan (- x) = - tan x.
+Proof.
+  intros x; unfold tan in |- *; rewrite sin_neg; rewrite cos_neg;
+    unfold Rdiv in |- *.
+  apply Ropp_mult_distr_l_reverse.
+Qed.
+
+Lemma tan_minus :
+  forall x y:R,
+    cos x <> 0 ->
+    cos y <> 0 ->
+    cos (x - y) <> 0 ->
+    1 + tan x * tan y <> 0 ->
+    tan (x - y) = (tan x - tan y) / (1 + tan x * tan y).
+Proof.
+  intros; unfold Rminus in |- *; rewrite tan_plus.
+  rewrite tan_neg; unfold Rminus in |- *; rewrite <- Ropp_mult_distr_l_reverse;
+    rewrite Rmult_opp_opp; reflexivity.
+  assumption.
+  rewrite cos_neg; assumption.
+  assumption.
+  rewrite tan_neg; unfold Rminus in |- *; rewrite <- Ropp_mult_distr_l_reverse;
+    rewrite Rmult_opp_opp; assumption.
+Qed.
+
+Lemma cos_3PI2 : cos (3 * (PI / 2)) = 0.
+Proof.
+  replace (3 * (PI / 2)) with (PI + PI / 2).
+  rewrite cos_plus; rewrite sin_PI; rewrite cos_PI2; ring.
+  pattern PI at 1 in |- *; rewrite (double_var PI).
+  ring.
+Qed.
+
+Lemma sin_2PI : sin (2 * PI) = 0.
+Proof.
+  rewrite sin_2a; rewrite sin_PI; ring.
+Qed.
+
+Lemma cos_2PI : cos (2 * PI) = 1.
+Proof.
+  rewrite cos_2a; rewrite sin_PI; rewrite cos_PI; ring.
+Qed.
+
+Lemma neg_sin : forall x:R, sin (x + PI) = - sin x.
+Proof.
+  intro x; rewrite sin_plus; rewrite sin_PI; rewrite cos_PI; ring.
+Qed.
+
+Lemma sin_PI_x : forall x:R, sin (PI - x) = sin x.
+Proof.
+  intro x; rewrite sin_minus; rewrite sin_PI; rewrite cos_PI; rewrite Rmult_0_l;
+    unfold Rminus in |- *; rewrite Rplus_0_l; rewrite Ropp_mult_distr_l_reverse;
+      rewrite Ropp_involutive; apply Rmult_1_l.
+Qed.
+
+Lemma sin_period : forall (x:R) (k:nat), sin (x + 2 * INR k * PI) = sin x.
+Proof.
+  intros x k; induction  k as [| k Hreck].
+  simpl in |- *;  ring_simplify (x + 2 * 0 * PI).
+  trivial.
+
+  replace (x + 2 * INR (S k) * PI) with (x + 2 * INR k * PI + 2 * PI).
+  rewrite sin_plus in |- *; rewrite sin_2PI in |- *; rewrite cos_2PI in |- *.
+  ring_simplify; trivial.
+  rewrite S_INR in |- *;  ring.
+Qed.
+
+Lemma cos_period : forall (x:R) (k:nat), cos (x + 2 * INR k * PI) = cos x.
+Proof.
+  intros x k; induction  k as [| k Hreck].
+  simpl in |- *;  ring_simplify (x + 2 * 0 * PI).
+  trivial.
+
+  replace (x + 2 * INR (S k) * PI) with (x + 2 * INR k * PI + 2 * PI).
+  rewrite cos_plus in |- *; rewrite sin_2PI in |- *; rewrite cos_2PI in |- *.
+  ring_simplify; trivial.
+  rewrite S_INR in |- *;  ring.
+Qed.
+
+Lemma sin_shift : forall x:R, sin (PI / 2 - x) = cos x.
+Proof.
+  intro x; rewrite sin_minus; rewrite sin_PI2; rewrite cos_PI2; ring.
+Qed.
+
+Lemma cos_shift : forall x:R, cos (PI / 2 - x) = sin x.
+Proof.
+  intro x; rewrite cos_minus; rewrite sin_PI2; rewrite cos_PI2; ring.
+Qed.
+
+Lemma cos_sin : forall x:R, cos x = sin (PI / 2 + x).
+Proof.
+  intro x; rewrite sin_plus; rewrite sin_PI2; rewrite cos_PI2; ring.
+Qed.
+
+Lemma PI2_RGT_0 : 0 < PI / 2.
+Proof.
+  unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+    [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup ].
+Qed.
+
+Lemma SIN_bound : forall x:R, -1 <= sin x <= 1.
+Proof.
+  intro; case (Rle_dec (-1) (sin x)); intro.
+  case (Rle_dec (sin x) 1); intro.
+  split; assumption.
+  cut (1 < sin x).
+  intro;
+    generalize
+      (Rsqr_incrst_1 1 (sin x) H (Rlt_le 0 1 Rlt_0_1)
+        (Rlt_le 0 (sin x) (Rlt_trans 0 1 (sin x) Rlt_0_1 H)));
+      rewrite Rsqr_1; intro; rewrite sin2 in H0; unfold Rminus in H0;
+        generalize (Rplus_lt_compat_l (-1) 1 (1 + - Rsqr (cos x)) H0);
+          repeat rewrite <- Rplus_assoc; repeat rewrite Rplus_opp_l;
+            rewrite Rplus_0_l; intro; rewrite <- Ropp_0 in H1;
+              generalize (Ropp_lt_gt_contravar (-0) (- Rsqr (cos x)) H1);
+                repeat rewrite Ropp_involutive; intro; generalize (Rle_0_sqr (cos x));
+                  intro; elim (Rlt_irrefl 0 (Rle_lt_trans 0 (Rsqr (cos x)) 0 H3 H2)).
+  auto with real.
+  cut (sin x < -1).
+  intro; generalize (Ropp_lt_gt_contravar (sin x) (-1) H);
+    rewrite Ropp_involutive; clear H; intro;
+      generalize
+        (Rsqr_incrst_1 1 (- sin x) H (Rlt_le 0 1 Rlt_0_1)
+          (Rlt_le 0 (- sin x) (Rlt_trans 0 1 (- sin x) Rlt_0_1 H)));
+        rewrite Rsqr_1; intro; rewrite <- Rsqr_neg in H0;
+          rewrite sin2 in H0; unfold Rminus in H0;
+            generalize (Rplus_lt_compat_l (-1) 1 (1 + - Rsqr (cos x)) H0);
+              repeat rewrite <- Rplus_assoc; repeat rewrite Rplus_opp_l;
+                rewrite Rplus_0_l; intro; rewrite <- Ropp_0 in H1;
+                  generalize (Ropp_lt_gt_contravar (-0) (- Rsqr (cos x)) H1);
+                    repeat rewrite Ropp_involutive; intro; generalize (Rle_0_sqr (cos x));
+                      intro; elim (Rlt_irrefl 0 (Rle_lt_trans 0 (Rsqr (cos x)) 0 H3 H2)).
+  auto with real.
+Qed.
+
+Lemma COS_bound : forall x:R, -1 <= cos x <= 1.
+Proof.
+  intro; rewrite <- sin_shift; apply SIN_bound.
+Qed.
+
+Lemma cos_sin_0 : forall x:R, ~ (cos x = 0 /\ sin x = 0).
+Proof.
+  intro; red in |- *; intro; elim H; intros; generalize (sin2_cos2 x); intro;
+    rewrite H0 in H2; rewrite H1 in H2; repeat rewrite Rsqr_0 in H2;
+      rewrite Rplus_0_r in H2; generalize Rlt_0_1; intro;
+        rewrite <- H2 in H3; elim (Rlt_irrefl 0 H3).
+Qed.
+
+Lemma cos_sin_0_var : forall x:R, cos x <> 0 \/ sin x <> 0.
+Proof.
+  intros x.
+  destruct (Req_dec (cos x) 0). 2: now left.
+  right. intros H'.
+  apply (cos_sin_0 x).
+  now split.
+Qed.
+
+(*****************************************************************)
+(** * Using series definitions of cos and sin                    *)
+(*****************************************************************)
+
+Definition sin_lb (a:R) : R := sin_approx a 3.
+Definition sin_ub (a:R) : R := sin_approx a 4.
+Definition cos_lb (a:R) : R := cos_approx a 3.
+Definition cos_ub (a:R) : R := cos_approx a 4.
+
+Lemma sin_lb_gt_0 : forall a:R, 0 < a -> a <= PI / 2 -> 0 < sin_lb a.
+Proof.
+  intros.
+  unfold sin_lb in |- *; unfold sin_approx in |- *; unfold sin_term in |- *.
+  set (Un := fun i:nat => a ^ (2 * i + 1) / INR (fact (2 * i + 1))).
+  replace
+  (sum_f_R0
+    (fun i:nat => (-1) ^ i * (a ^ (2 * i + 1) / INR (fact (2 * i + 1)))) 3)
+    with (sum_f_R0 (fun i:nat => (-1) ^ i * Un i) 3);
+      [ idtac | apply sum_eq; intros; unfold Un in |- *; reflexivity ].
+  cut (forall n:nat, Un (S n) < Un n).
+  intro; simpl in |- *.
+  repeat rewrite Rmult_1_l; repeat rewrite Rmult_1_r;
+    replace (-1 * Un 1%nat) with (- Un 1%nat); [ idtac | ring ];
+    replace (-1 * -1 * Un 2%nat) with (Un 2%nat); [ idtac | ring ];
+    replace (-1 * (-1 * -1) * Un 3%nat) with (- Un 3%nat);
+    [ idtac | ring ];
+    replace (Un 0%nat + - Un 1%nat + Un 2%nat + - Un 3%nat) with
+    (Un 0%nat - Un 1%nat + (Un 2%nat - Un 3%nat)); [ idtac | ring ].
+  apply Rplus_lt_0_compat.
+  unfold Rminus in |- *; apply Rplus_lt_reg_r with (Un 1%nat);
+    rewrite Rplus_0_r; rewrite (Rplus_comm (Un 1%nat));
+      rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r;
+        apply H1.
+  unfold Rminus in |- *; apply Rplus_lt_reg_r with (Un 3%nat);
+    rewrite Rplus_0_r; rewrite (Rplus_comm (Un 3%nat));
+      rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r;
+        apply H1.
+  intro; unfold Un in |- *.
+  cut ((2 * S n + 1)%nat = (2 * n + 1 + 2)%nat).
+  intro; rewrite H1.
+  rewrite pow_add; unfold Rdiv in |- *; rewrite Rmult_assoc;
+    apply Rmult_lt_compat_l.
+  apply pow_lt; assumption.
+  rewrite <- H1; apply Rmult_lt_reg_l with (INR (fact (2 * n + 1))).
+  apply lt_INR_0; apply neq_O_lt.
+  assert (H2 := fact_neq_0 (2 * n + 1)).
+  red in |- *; intro; elim H2; symmetry  in |- *; assumption.
+  rewrite <- Rinv_r_sym.
+  apply Rmult_lt_reg_l with (INR (fact (2 * S n + 1))).
+  apply lt_INR_0; apply neq_O_lt.
+  assert (H2 := fact_neq_0 (2 * S n + 1)).
+  red in |- *; intro; elim H2; symmetry  in |- *; assumption.
+  rewrite (Rmult_comm (INR (fact (2 * S n + 1)))); repeat rewrite Rmult_assoc;
+    rewrite <- Rinv_l_sym.
+  do 2 rewrite Rmult_1_r; apply Rle_lt_trans with (INR (fact (2 * n + 1)) * 4).
+  apply Rmult_le_compat_l.
+  replace 0 with (INR 0); [ idtac | reflexivity ]; apply le_INR; apply le_O_n.
+  simpl in |- *; rewrite Rmult_1_r; replace 4 with (Rsqr 2);
+    [ idtac | ring_Rsqr ]; replace (a * a) with (Rsqr a);
+    [ idtac | reflexivity ]; apply Rsqr_incr_1.
+  apply Rle_trans with (PI / 2);
+    [ assumption
+      | unfold Rdiv in |- *; apply Rmult_le_reg_l with 2;
+        [ prove_sup0
+          | rewrite <- Rmult_assoc; rewrite Rinv_r_simpl_m;
+            [ replace 4 with 4; [ apply PI_4 | ring ] | discrR ] ] ].
+  left; assumption.
+  left; prove_sup0.
+  rewrite H1; replace (2 * n + 1 + 2)%nat with (S (S (2 * n + 1))).
+  do 2 rewrite fact_simpl; do 2 rewrite mult_INR.
+  repeat rewrite <- Rmult_assoc.
+  rewrite <- (Rmult_comm (INR (fact (2 * n + 1)))).
+  rewrite Rmult_assoc.
+  apply Rmult_lt_compat_l.
+  apply lt_INR_0; apply neq_O_lt.
+  assert (H2 := fact_neq_0 (2 * n + 1)).
+  red in |- *; intro; elim H2; symmetry  in |- *; assumption.
+  do 2 rewrite S_INR; rewrite plus_INR; rewrite mult_INR; set (x := INR n);
+    unfold INR in |- *.
+  replace ((2 * x + 1 + 1 + 1) * (2 * x + 1 + 1)) with (4 * x * x + 10 * x + 6);
+  [ idtac | ring ].
+  apply Rplus_lt_reg_r with (-4); rewrite Rplus_opp_l;
+    replace (-4 + (4 * x * x + 10 * x + 6)) with (4 * x * x + 10 * x + 2);
+    [ idtac | ring ].
+  apply Rplus_le_lt_0_compat.
+  cut (0 <= x).
+  intro; apply Rplus_le_le_0_compat; repeat apply Rmult_le_pos;
+    assumption || left; prove_sup.
+  unfold x in |- *; replace 0 with (INR 0);
+    [ apply le_INR; apply le_O_n | reflexivity ].
+  prove_sup0.
+  ring.
+  apply INR_fact_neq_0.
+  apply INR_fact_neq_0.
+  ring.
+Qed.
+
+Lemma SIN : forall a:R, 0 <= a -> a <= PI -> sin_lb a <= sin a <= sin_ub a.
+  intros; unfold sin_lb, sin_ub in |- *; apply (sin_bound a 1 H H0).
+Qed.
+
+Lemma COS :
+  forall a:R, - PI / 2 <= a -> a <= PI / 2 -> cos_lb a <= cos a <= cos_ub a.
+  intros; unfold cos_lb, cos_ub in |- *; apply (cos_bound a 1 H H0).
+Qed.
+
+(**********)
+Lemma _PI2_RLT_0 : - (PI / 2) < 0.
+Proof.
+  rewrite <- Ropp_0; apply Ropp_lt_contravar; apply PI2_RGT_0.
+Qed.
+
+Lemma PI4_RLT_PI2 : PI / 4 < PI / 2.
+Proof.
+  unfold Rdiv in |- *; apply Rmult_lt_compat_l.
+  apply PI_RGT_0.
+  apply Rinv_lt_contravar.
+  apply Rmult_lt_0_compat; prove_sup0.
+  pattern 2 at 1 in |- *; rewrite <- Rplus_0_r.
+  replace 4 with (2 + 2); [ apply Rplus_lt_compat_l; prove_sup0 | ring ].
+Qed.
+
+Lemma PI2_Rlt_PI : PI / 2 < PI.
+Proof.
+  unfold Rdiv in |- *; pattern PI at 2 in |- *; rewrite <- Rmult_1_r.
+  apply Rmult_lt_compat_l.
+  apply PI_RGT_0.
+  pattern 1 at 3 in |- *; rewrite <- Rinv_1; apply Rinv_lt_contravar.
+  rewrite Rmult_1_l; prove_sup0.
+  pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
+    apply Rlt_0_1.
+Qed.
+
+(***************************************************)
+(** * Increasing and decreasing of [cos] and [sin] *)
+(***************************************************)
+Theorem sin_gt_0 : forall x:R, 0 < x -> x < PI -> 0 < sin x.
+Proof.
+  intros; elim (SIN x (Rlt_le 0 x H) (Rlt_le x PI H0)); intros H1 _;
+    case (Rtotal_order x (PI / 2)); intro H2.
+  apply Rlt_le_trans with (sin_lb x).
+  apply sin_lb_gt_0; [ assumption | left; assumption ].
+  assumption.
+  elim H2; intro H3.
+  rewrite H3; rewrite sin_PI2; apply Rlt_0_1.
+  rewrite <- sin_PI_x; generalize (Ropp_gt_lt_contravar x (PI / 2) H3);
+    intro H4; generalize (Rplus_lt_compat_l PI (- x) (- (PI / 2)) H4).
+  replace (PI + - x) with (PI - x).
+  replace (PI + - (PI / 2)) with (PI / 2).
+  intro H5; generalize (Ropp_lt_gt_contravar x PI H0); intro H6;
+    change (- PI < - x) in H6; generalize (Rplus_lt_compat_l PI (- PI) (- x) H6).
+  rewrite Rplus_opp_r.
+  replace (PI + - x) with (PI - x).
+  intro H7;
+    elim
+      (SIN (PI - x) (Rlt_le 0 (PI - x) H7)
+        (Rlt_le (PI - x) PI (Rlt_trans (PI - x) (PI / 2) PI H5 PI2_Rlt_PI)));
+      intros H8 _;
+        generalize (sin_lb_gt_0 (PI - x) H7 (Rlt_le (PI - x) (PI / 2) H5));
+          intro H9; apply (Rlt_le_trans 0 (sin_lb (PI - x)) (sin (PI - x)) H9 H8).
+  reflexivity.
+  pattern PI at 2 in |- *; rewrite double_var; ring.
+  reflexivity.
+Qed.
+
+Theorem cos_gt_0 : forall x:R, - (PI / 2) < x -> x < PI / 2 -> 0 < cos x.
+Proof.
+  intros; rewrite cos_sin;
+    generalize (Rplus_lt_compat_l (PI / 2) (- (PI / 2)) x H).
+  rewrite Rplus_opp_r; intro H1;
+    generalize (Rplus_lt_compat_l (PI / 2) x (PI / 2) H0);
+      rewrite <- double_var; intro H2; apply (sin_gt_0 (PI / 2 + x) H1 H2).
+Qed.
+
+Lemma sin_ge_0 : forall x:R, 0 <= x -> x <= PI -> 0 <= sin x.
+Proof.
+  intros x H1 H2; elim H1; intro H3;
+    [ elim H2; intro H4;
+      [ left; apply (sin_gt_0 x H3 H4)
+        | rewrite H4; right; symmetry  in |- *; apply sin_PI ]
+      | rewrite <- H3; right; symmetry  in |- *; apply sin_0 ].
+Qed.
+
+Lemma cos_ge_0 : forall x:R, - (PI / 2) <= x -> x <= PI / 2 -> 0 <= cos x.
+Proof.
+  intros x H1 H2; elim H1; intro H3;
+    [ elim H2; intro H4;
+      [ left; apply (cos_gt_0 x H3 H4)
+        | rewrite H4; right; symmetry  in |- *; apply cos_PI2 ]
+      | rewrite <- H3; rewrite cos_neg; right; symmetry  in |- *; apply cos_PI2 ].
+Qed.
+
+Lemma sin_le_0 : forall x:R, PI <= x -> x <= 2 * PI -> sin x <= 0.
+Proof.
+  intros x H1 H2; apply Rge_le; rewrite <- Ropp_0;
+    rewrite <- (Ropp_involutive (sin x)); apply Ropp_le_ge_contravar;
+      rewrite <- neg_sin; replace (x + PI) with (x - PI + 2 * INR 1 * PI);
+        [ rewrite (sin_period (x - PI) 1); apply sin_ge_0;
+          [ replace (x - PI) with (x + - PI);
+            [ rewrite Rplus_comm; replace 0 with (- PI + PI);
+              [ apply Rplus_le_compat_l; assumption | ring ]
+              | ring ]
+            | replace (x - PI) with (x + - PI); rewrite Rplus_comm;
+              [ pattern PI at 2 in |- *; replace PI with (- PI + 2 * PI);
+                [ apply Rplus_le_compat_l; assumption | ring ]
+                | ring ] ]
+          | unfold INR in |- *; ring ].
+Qed.
+
+Lemma cos_le_0 : forall x:R, PI / 2 <= x -> x <= 3 * (PI / 2) -> cos x <= 0.
+Proof.
+  intros x H1 H2; apply Rge_le; rewrite <- Ropp_0;
+    rewrite <- (Ropp_involutive (cos x)); apply Ropp_le_ge_contravar;
+      rewrite <- neg_cos; replace (x + PI) with (x - PI + 2 * INR 1 * PI).
+  rewrite cos_period; apply cos_ge_0.
+  replace (- (PI / 2)) with (- PI + PI / 2).
+  unfold Rminus in |- *; rewrite (Rplus_comm x); apply Rplus_le_compat_l;
+    assumption.
+  pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr;
+    ring.
+  unfold Rminus in |- *; rewrite Rplus_comm;
+    replace (PI / 2) with (- PI + 3 * (PI / 2)).
+  apply Rplus_le_compat_l; assumption.
+  pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr;
+    ring.
+  unfold INR in |- *; ring.
+Qed.
+
+Lemma sin_lt_0 : forall x:R, PI < x -> x < 2 * PI -> sin x < 0.
+Proof.
+  intros x H1 H2; rewrite <- Ropp_0; rewrite <- (Ropp_involutive (sin x));
+    apply Ropp_lt_gt_contravar; rewrite <- neg_sin;
+      replace (x + PI) with (x - PI + 2 * INR 1 * PI);
+      [ rewrite (sin_period (x - PI) 1); apply sin_gt_0;
+        [ replace (x - PI) with (x + - PI);
+          [ rewrite Rplus_comm; replace 0 with (- PI + PI);
+            [ apply Rplus_lt_compat_l; assumption | ring ]
+            | ring ]
+          | replace (x - PI) with (x + - PI); rewrite Rplus_comm;
+            [ pattern PI at 2 in |- *; replace PI with (- PI + 2 * PI);
+              [ apply Rplus_lt_compat_l; assumption | ring ]
+              | ring ] ]
+        | unfold INR in |- *; ring ].
+Qed.
+
+Lemma sin_lt_0_var : forall x:R, - PI < x -> x < 0 -> sin x < 0.
+Proof.
+  intros; generalize (Rplus_lt_compat_l (2 * PI) (- PI) x H);
+    replace (2 * PI + - PI) with PI;
+    [ intro H1; rewrite Rplus_comm in H1;
+      generalize (Rplus_lt_compat_l (2 * PI) x 0 H0);
+        intro H2; rewrite (Rplus_comm (2 * PI)) in H2;
+          rewrite <- (Rplus_comm 0) in H2; rewrite Rplus_0_l in H2;
+            rewrite <- (sin_period x 1); unfold INR in |- *;
+              replace (2 * 1 * PI) with (2 * PI);
+              [ apply (sin_lt_0 (x + 2 * PI) H1 H2) | ring ]
+      | ring ].
+Qed.
+
+Lemma cos_lt_0 : forall x:R, PI / 2 < x -> x < 3 * (PI / 2) -> cos x < 0.
+Proof.
+  intros x H1 H2; rewrite <- Ropp_0; rewrite <- (Ropp_involutive (cos x));
+    apply Ropp_lt_gt_contravar; rewrite <- neg_cos;
+      replace (x + PI) with (x - PI + 2 * INR 1 * PI).
+  rewrite cos_period; apply cos_gt_0.
+  replace (- (PI / 2)) with (- PI + PI / 2).
+  unfold Rminus in |- *; rewrite (Rplus_comm x); apply Rplus_lt_compat_l;
+    assumption.
+  pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr;
+    ring.
+  unfold Rminus in |- *; rewrite Rplus_comm;
+    replace (PI / 2) with (- PI + 3 * (PI / 2)).
+  apply Rplus_lt_compat_l; assumption.
+  pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr;
+    ring.
+  unfold INR in |- *; ring.
+Qed.
+
+Lemma tan_gt_0 : forall x:R, 0 < x -> x < PI / 2 -> 0 < tan x.
+Proof.
+  intros x H1 H2; unfold tan in |- *; generalize _PI2_RLT_0;
+    generalize (Rlt_trans 0 x (PI / 2) H1 H2); intros;
+      generalize (Rlt_trans (- (PI / 2)) 0 x H0 H1); intro H5;
+        generalize (Rlt_trans x (PI / 2) PI H2 PI2_Rlt_PI);
+          intro H7; unfold Rdiv in |- *; apply Rmult_lt_0_compat.
+  apply sin_gt_0; assumption.
+  apply Rinv_0_lt_compat; apply cos_gt_0; assumption.
+Qed.
+
+Lemma tan_lt_0 : forall x:R, - (PI / 2) < x -> x < 0 -> tan x < 0.
+Proof.
+  intros x H1 H2; unfold tan in |- *;
+    generalize (cos_gt_0 x H1 (Rlt_trans x 0 (PI / 2) H2 PI2_RGT_0));
+      intro H3; rewrite <- Ropp_0;
+        replace (sin x / cos x) with (- (- sin x / cos x)).
+  rewrite <- sin_neg; apply Ropp_gt_lt_contravar;
+    change (0 < sin (- x) / cos x) in |- *; unfold Rdiv in |- *;
+      apply Rmult_lt_0_compat.
+  apply sin_gt_0.
+  rewrite <- Ropp_0; apply Ropp_gt_lt_contravar; assumption.
+  apply Rlt_trans with (PI / 2).
+  rewrite <- (Ropp_involutive (PI / 2)); apply Ropp_gt_lt_contravar; assumption.
+  apply PI2_Rlt_PI.
+  apply Rinv_0_lt_compat; assumption.
+  unfold Rdiv in |- *; ring.
+Qed.
+
+Lemma cos_ge_0_3PI2 :
+  forall x:R, 3 * (PI / 2) <= x -> x <= 2 * PI -> 0 <= cos x.
+Proof.
+  intros; rewrite <- cos_neg; rewrite <- (cos_period (- x) 1);
+    unfold INR in |- *; replace (- x + 2 * 1 * PI) with (2 * PI - x).
+  generalize (Ropp_le_ge_contravar x (2 * PI) H0); intro H1;
+    generalize (Rge_le (- x) (- (2 * PI)) H1); clear H1;
+      intro H1; generalize (Rplus_le_compat_l (2 * PI) (- (2 * PI)) (- x) H1).
+  rewrite Rplus_opp_r.
+  intro H2; generalize (Ropp_le_ge_contravar (3 * (PI / 2)) x H); intro H3;
+    generalize (Rge_le (- (3 * (PI / 2))) (- x) H3); clear H3;
+      intro H3;
+        generalize (Rplus_le_compat_l (2 * PI) (- x) (- (3 * (PI / 2))) H3).
+  replace (2 * PI + - (3 * (PI / 2))) with (PI / 2).
+  intro H4;
+    apply
+      (cos_ge_0 (2 * PI - x)
+        (Rlt_le (- (PI / 2)) (2 * PI - x)
+          (Rlt_le_trans (- (PI / 2)) 0 (2 * PI - x) _PI2_RLT_0 H2)) H4).
+  rewrite double; pattern PI at 2 3 in |- *; rewrite double_var; ring.
+  ring.
+Qed.
+
+Lemma form1 :
+  forall p q:R, cos p + cos q = 2 * cos ((p - q) / 2) * cos ((p + q) / 2).
+Proof.
+  intros p q; pattern p at 1 in |- *;
+    replace p with ((p - q) / 2 + (p + q) / 2).
+  rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2).
+  rewrite cos_plus; rewrite cos_minus; ring.
+  pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring.
+  pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring.
+Qed.
+
+Lemma form2 :
+  forall p q:R, cos p - cos q = -2 * sin ((p - q) / 2) * sin ((p + q) / 2).
+Proof.
+  intros p q; pattern p at 1 in |- *;
+    replace p with ((p - q) / 2 + (p + q) / 2).
+  rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2).
+  rewrite cos_plus; rewrite cos_minus; ring.
+  pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring.
+  pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring.
+Qed.
+
+Lemma form3 :
+  forall p q:R, sin p + sin q = 2 * cos ((p - q) / 2) * sin ((p + q) / 2).
+Proof.
+  intros p q; pattern p at 1 in |- *;
+    replace p with ((p - q) / 2 + (p + q) / 2).
+  pattern q at 3 in |- *; replace q with ((p + q) / 2 - (p - q) / 2).
+  rewrite sin_plus; rewrite sin_minus; ring.
+  pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring.
+  pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring.
+Qed.
+
+Lemma form4 :
+  forall p q:R, sin p - sin q = 2 * cos ((p + q) / 2) * sin ((p - q) / 2).
+Proof.
+  intros p q; pattern p at 1 in |- *;
+    replace p with ((p - q) / 2 + (p + q) / 2).
+  pattern q at 3 in |- *; replace q with ((p + q) / 2 - (p - q) / 2).
+  rewrite sin_plus; rewrite sin_minus; ring.
+  pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring.
+  pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring.
+
+Qed.
+
+Lemma sin_increasing_0 :
+  forall x y:R,
+    - (PI / 2) <= x ->
+    x <= PI / 2 -> - (PI / 2) <= y -> y <= PI / 2 -> sin x < sin y -> x < y.
+Proof.
+  intros; cut (sin ((x - y) / 2) < 0).
+  intro H4; case (Rtotal_order ((x - y) / 2) 0); intro H5.
+  assert (Hyp : 0 < 2).
+  prove_sup0.
+  generalize (Rmult_lt_compat_l 2 ((x - y) / 2) 0 Hyp H5).
+  unfold Rdiv in |- *.
+  rewrite <- Rmult_assoc.
+  rewrite Rinv_r_simpl_m.
+  rewrite Rmult_0_r.
+  clear H5; intro H5; apply Rminus_lt; assumption.
+  discrR.
+  elim H5; intro H6.
+  rewrite H6 in H4; rewrite sin_0 in H4; elim (Rlt_irrefl 0 H4).
+  change (0 < (x - y) / 2) in H6;
+    generalize (Ropp_le_ge_contravar (- (PI / 2)) y H1).
+  rewrite Ropp_involutive.
+  intro H7; generalize (Rge_le (PI / 2) (- y) H7); clear H7; intro H7;
+    generalize (Rplus_le_compat x (PI / 2) (- y) (PI / 2) H0 H7).
+  rewrite <- double_var.
+  intro H8.
+  assert (Hyp : 0 < 2).
+  prove_sup0.
+  generalize
+    (Rmult_le_compat_l (/ 2) (x - y) PI
+      (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H8).
+  repeat rewrite (Rmult_comm (/ 2)).
+  intro H9;
+    generalize
+      (sin_gt_0 ((x - y) / 2) H6
+        (Rle_lt_trans ((x - y) / 2) (PI / 2) PI H9 PI2_Rlt_PI));
+      intro H10;
+        elim
+          (Rlt_irrefl (sin ((x - y) / 2))
+            (Rlt_trans (sin ((x - y) / 2)) 0 (sin ((x - y) / 2)) H4 H10)).
+  generalize (Rlt_minus (sin x) (sin y) H3); clear H3; intro H3;
+    rewrite form4 in H3;
+      generalize (Rplus_le_compat x (PI / 2) y (PI / 2) H0 H2).
+  rewrite <- double_var.
+  assert (Hyp : 0 < 2).
+  prove_sup0.
+  intro H4;
+    generalize
+      (Rmult_le_compat_l (/ 2) (x + y) PI
+        (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H4).
+  repeat rewrite (Rmult_comm (/ 2)).
+  clear H4; intro H4;
+    generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) y H H1);
+      replace (- (PI / 2) + - (PI / 2)) with (- PI).
+  intro H5;
+    generalize
+      (Rmult_le_compat_l (/ 2) (- PI) (x + y)
+        (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H5).
+  replace (/ 2 * (x + y)) with ((x + y) / 2).
+  replace (/ 2 * - PI) with (- (PI / 2)).
+  clear H5; intro H5; elim H4; intro H40.
+  elim H5; intro H50.
+  generalize (cos_gt_0 ((x + y) / 2) H50 H40); intro H6;
+    generalize (Rmult_lt_compat_l 2 0 (cos ((x + y) / 2)) Hyp H6).
+  rewrite Rmult_0_r.
+  clear H6; intro H6; case (Rcase_abs (sin ((x - y) / 2))); intro H7.
+  assumption.
+  generalize (Rge_le (sin ((x - y) / 2)) 0 H7); clear H7; intro H7;
+    generalize
+      (Rmult_le_pos (2 * cos ((x + y) / 2)) (sin ((x - y) / 2))
+        (Rlt_le 0 (2 * cos ((x + y) / 2)) H6) H7); intro H8;
+      generalize
+        (Rle_lt_trans 0 (2 * cos ((x + y) / 2) * sin ((x - y) / 2)) 0 H8 H3);
+        intro H9; elim (Rlt_irrefl 0 H9).
+  rewrite <- H50 in H3; rewrite cos_neg in H3; rewrite cos_PI2 in H3;
+    rewrite Rmult_0_r in H3; rewrite Rmult_0_l in H3;
+      elim (Rlt_irrefl 0 H3).
+  unfold Rdiv in H3.
+  rewrite H40 in H3; assert (H50 := cos_PI2); unfold Rdiv in H50;
+    rewrite H50 in H3; rewrite Rmult_0_r in H3; rewrite Rmult_0_l in H3;
+      elim (Rlt_irrefl 0 H3).
+  unfold Rdiv in |- *.
+  rewrite <- Ropp_mult_distr_l_reverse.
+  apply Rmult_comm.
+  unfold Rdiv in |- *; apply Rmult_comm.
+  pattern PI at 1 in |- *; rewrite double_var.
+  rewrite Ropp_plus_distr.
+  reflexivity.
+Qed.
+
+Lemma sin_increasing_1 :
+  forall x y:R,
+    - (PI / 2) <= x ->
+    x <= PI / 2 -> - (PI / 2) <= y -> y <= PI / 2 -> x < y -> sin x < sin y.
+Proof.
+  intros; generalize (Rplus_lt_compat_l x x y H3); intro H4;
+    generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) x H H);
+      replace (- (PI / 2) + - (PI / 2)) with (- PI).
+  assert (Hyp : 0 < 2).
+  prove_sup0.
+  intro H5; generalize (Rle_lt_trans (- PI) (x + x) (x + y) H5 H4); intro H6;
+    generalize
+      (Rmult_lt_compat_l (/ 2) (- PI) (x + y) (Rinv_0_lt_compat 2 Hyp) H6);
+      replace (/ 2 * - PI) with (- (PI / 2)).
+  replace (/ 2 * (x + y)) with ((x + y) / 2).
+  clear H4 H5 H6; intro H4; generalize (Rplus_lt_compat_l y x y H3); intro H5;
+    rewrite Rplus_comm in H5;
+      generalize (Rplus_le_compat y (PI / 2) y (PI / 2) H2 H2).
+  rewrite <- double_var.
+  intro H6; generalize (Rlt_le_trans (x + y) (y + y) PI H5 H6); intro H7;
+    generalize (Rmult_lt_compat_l (/ 2) (x + y) PI (Rinv_0_lt_compat 2 Hyp) H7);
+      replace (/ 2 * PI) with (PI / 2).
+  replace (/ 2 * (x + y)) with ((x + y) / 2).
+  clear H5 H6 H7; intro H5; generalize (Ropp_le_ge_contravar (- (PI / 2)) y H1);
+    rewrite Ropp_involutive; clear H1; intro H1;
+      generalize (Rge_le (PI / 2) (- y) H1); clear H1; intro H1;
+        generalize (Ropp_le_ge_contravar y (PI / 2) H2); clear H2;
+          intro H2; generalize (Rge_le (- y) (- (PI / 2)) H2);
+            clear H2; intro H2; generalize (Rplus_lt_compat_l (- y) x y H3);
+              replace (- y + x) with (x - y).
+  rewrite Rplus_opp_l.
+  intro H6;
+    generalize (Rmult_lt_compat_l (/ 2) (x - y) 0 (Rinv_0_lt_compat 2 Hyp) H6);
+      rewrite Rmult_0_r; replace (/ 2 * (x - y)) with ((x - y) / 2).
+  clear H6; intro H6;
+    generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) (- y) H H2);
+      replace (- (PI / 2) + - (PI / 2)) with (- PI).
+  replace (x + - y) with (x - y).
+  intro H7;
+    generalize
+      (Rmult_le_compat_l (/ 2) (- PI) (x - y)
+        (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H7);
+      replace (/ 2 * - PI) with (- (PI / 2)).
+  replace (/ 2 * (x - y)) with ((x - y) / 2).
+  clear H7; intro H7; clear H H0 H1 H2; apply Rminus_lt; rewrite form4;
+    generalize (cos_gt_0 ((x + y) / 2) H4 H5); intro H8;
+      generalize (Rmult_lt_0_compat 2 (cos ((x + y) / 2)) Hyp H8);
+        clear H8; intro H8; cut (- PI < - (PI / 2)).
+  intro H9;
+    generalize
+      (sin_lt_0_var ((x - y) / 2)
+        (Rlt_le_trans (- PI) (- (PI / 2)) ((x - y) / 2) H9 H7) H6);
+      intro H10;
+        generalize
+          (Rmult_lt_gt_compat_neg_l (sin ((x - y) / 2)) 0 (
+            2 * cos ((x + y) / 2)) H10 H8); intro H11; rewrite Rmult_0_r in H11;
+          rewrite Rmult_comm; assumption.
+  apply Ropp_lt_gt_contravar; apply PI2_Rlt_PI.
+  unfold Rdiv in |- *; apply Rmult_comm.
+  unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse; apply Rmult_comm.
+  reflexivity.
+  pattern PI at 1 in |- *; rewrite double_var.
+  rewrite Ropp_plus_distr.
+  reflexivity.
+  unfold Rdiv in |- *; apply Rmult_comm.
+  unfold Rminus in |- *; apply Rplus_comm.
+  unfold Rdiv in |- *; apply Rmult_comm.
+  unfold Rdiv in |- *; apply Rmult_comm.
+  unfold Rdiv in |- *; apply Rmult_comm.
+  unfold Rdiv in |- *.
+  rewrite <- Ropp_mult_distr_l_reverse.
+  apply Rmult_comm.
+  pattern PI at 1 in |- *; rewrite double_var.
+  rewrite Ropp_plus_distr.
+  reflexivity.
+Qed.
+
+Lemma sin_decreasing_0 :
+  forall x y:R,
+    x <= 3 * (PI / 2) ->
+    PI / 2 <= x -> y <= 3 * (PI / 2) -> PI / 2 <= y -> sin x < sin y -> y < x.
+Proof.
+  intros; rewrite <- (sin_PI_x x) in H3; rewrite <- (sin_PI_x y) in H3;
+    generalize (Ropp_lt_gt_contravar (sin (PI - x)) (sin (PI - y)) H3);
+      repeat rewrite <- sin_neg;
+        generalize (Rplus_le_compat_l (- PI) x (3 * (PI / 2)) H);
+          generalize (Rplus_le_compat_l (- PI) (PI / 2) x H0);
+            generalize (Rplus_le_compat_l (- PI) y (3 * (PI / 2)) H1);
+              generalize (Rplus_le_compat_l (- PI) (PI / 2) y H2);
+                replace (- PI + x) with (x - PI).
+  replace (- PI + PI / 2) with (- (PI / 2)).
+  replace (- PI + y) with (y - PI).
+  replace (- PI + 3 * (PI / 2)) with (PI / 2).
+  replace (- (PI - x)) with (x - PI).
+  replace (- (PI - y)) with (y - PI).
+  intros; change (sin (y - PI) < sin (x - PI)) in H8;
+    apply Rplus_lt_reg_r with (- PI); rewrite Rplus_comm;
+      replace (y + - PI) with (y - PI).
+  rewrite Rplus_comm; replace (x + - PI) with (x - PI).
+  apply (sin_increasing_0 (y - PI) (x - PI) H4 H5 H6 H7 H8).
+  reflexivity.
+  reflexivity.
+  unfold Rminus in |- *; rewrite Ropp_plus_distr.
+  rewrite Ropp_involutive.
+  apply Rplus_comm.
+  unfold Rminus in |- *; rewrite Ropp_plus_distr.
+  rewrite Ropp_involutive.
+  apply Rplus_comm.
+  pattern PI at 2 in |- *; rewrite double_var.
+  rewrite Ropp_plus_distr.
+  ring.
+  unfold Rminus in |- *; apply Rplus_comm.
+  pattern PI at 2 in |- *; rewrite double_var.
+  rewrite Ropp_plus_distr.
+  ring.
+  unfold Rminus in |- *; apply Rplus_comm.
+Qed.
+
+Lemma sin_decreasing_1 :
+  forall x y:R,
+    x <= 3 * (PI / 2) ->
+    PI / 2 <= x -> y <= 3 * (PI / 2) -> PI / 2 <= y -> x < y -> sin y < sin x.
+Proof.
+  intros; rewrite <- (sin_PI_x x); rewrite <- (sin_PI_x y);
+    generalize (Rplus_le_compat_l (- PI) x (3 * (PI / 2)) H);
+      generalize (Rplus_le_compat_l (- PI) (PI / 2) x H0);
+        generalize (Rplus_le_compat_l (- PI) y (3 * (PI / 2)) H1);
+          generalize (Rplus_le_compat_l (- PI) (PI / 2) y H2);
+            generalize (Rplus_lt_compat_l (- PI) x y H3);
+              replace (- PI + PI / 2) with (- (PI / 2)).
+  replace (- PI + y) with (y - PI).
+  replace (- PI + 3 * (PI / 2)) with (PI / 2).
+  replace (- PI + x) with (x - PI).
+  intros; apply Ropp_lt_cancel; repeat rewrite <- sin_neg;
+    replace (- (PI - x)) with (x - PI).
+  replace (- (PI - y)) with (y - PI).
+  apply (sin_increasing_1 (x - PI) (y - PI) H7 H8 H5 H6 H4).
+  unfold Rminus in |- *; rewrite Ropp_plus_distr.
+  rewrite Ropp_involutive.
+  apply Rplus_comm.
+  unfold Rminus in |- *; rewrite Ropp_plus_distr.
+  rewrite Ropp_involutive.
+  apply Rplus_comm.
+  unfold Rminus in |- *; apply Rplus_comm.
+  pattern PI at 2 in |- *; rewrite double_var; ring.
+  unfold Rminus in |- *; apply Rplus_comm.
+  pattern PI at 2 in |- *; rewrite double_var; ring.
+Qed.
+
+Lemma cos_increasing_0 :
+  forall x y:R,
+    PI <= x -> x <= 2 * PI -> PI <= y -> y <= 2 * PI -> cos x < cos y -> x < y.
+Proof.
+  intros x y H1 H2 H3 H4; rewrite <- (cos_neg x); rewrite <- (cos_neg y);
+    rewrite <- (cos_period (- x) 1); rewrite <- (cos_period (- y) 1);
+      unfold INR in |- *;
+        replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))).
+  replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))).
+  repeat rewrite cos_shift; intro H5;
+    generalize (Rplus_le_compat_l (-3 * (PI / 2)) PI x H1);
+      generalize (Rplus_le_compat_l (-3 * (PI / 2)) x (2 * PI) H2);
+        generalize (Rplus_le_compat_l (-3 * (PI / 2)) PI y H3);
+          generalize (Rplus_le_compat_l (-3 * (PI / 2)) y (2 * PI) H4).
+  replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)).
+  replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)).
+  replace (-3 * (PI / 2) + 2 * PI) with (PI / 2).
+  replace (-3 * (PI / 2) + PI) with (- (PI / 2)).
+  clear H1 H2 H3 H4; intros H1 H2 H3 H4;
+    apply Rplus_lt_reg_r with (-3 * (PI / 2));
+      replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)).
+  replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)).
+  apply (sin_increasing_0 (x - 3 * (PI / 2)) (y - 3 * (PI / 2)) H4 H3 H2 H1 H5).
+  unfold Rminus in |- *.
+  rewrite Ropp_mult_distr_l_reverse.
+  apply Rplus_comm.
+  unfold Rminus in |- *.
+  rewrite Ropp_mult_distr_l_reverse.
+  apply Rplus_comm.
+  pattern PI at 3 in |- *; rewrite double_var.
+  ring.
+  rewrite double; pattern PI at 3 4 in |- *; rewrite double_var.
+  ring.
+  unfold Rminus in |- *.
+  rewrite Ropp_mult_distr_l_reverse.
+  apply Rplus_comm.
+  unfold Rminus in |- *.
+  rewrite Ropp_mult_distr_l_reverse.
+  apply Rplus_comm.
+  rewrite Rmult_1_r.
+  rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var.
+  ring.
+  rewrite Rmult_1_r.
+  rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var.
+  ring.
+Qed.
+
+Lemma cos_increasing_1 :
+  forall x y:R,
+    PI <= x -> x <= 2 * PI -> PI <= y -> y <= 2 * PI -> x < y -> cos x < cos y.
+Proof.
+  intros x y H1 H2 H3 H4 H5;
+    generalize (Rplus_le_compat_l (-3 * (PI / 2)) PI x H1);
+      generalize (Rplus_le_compat_l (-3 * (PI / 2)) x (2 * PI) H2);
+        generalize (Rplus_le_compat_l (-3 * (PI / 2)) PI y H3);
+          generalize (Rplus_le_compat_l (-3 * (PI / 2)) y (2 * PI) H4);
+            generalize (Rplus_lt_compat_l (-3 * (PI / 2)) x y H5);
+              rewrite <- (cos_neg x); rewrite <- (cos_neg y);
+                rewrite <- (cos_period (- x) 1); rewrite <- (cos_period (- y) 1);
+                  unfold INR in |- *; replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)).
+  replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)).
+  replace (-3 * (PI / 2) + PI) with (- (PI / 2)).
+  replace (-3 * (PI / 2) + 2 * PI) with (PI / 2).
+  clear H1 H2 H3 H4 H5; intros H1 H2 H3 H4 H5;
+    replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))).
+  replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))).
+  repeat rewrite cos_shift;
+    apply
+      (sin_increasing_1 (x - 3 * (PI / 2)) (y - 3 * (PI / 2)) H5 H4 H3 H2 H1).
+  rewrite Rmult_1_r.
+  rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var.
+  ring.
+  rewrite Rmult_1_r.
+  rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var.
+  ring.
+  rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var.
+  ring.
+  pattern PI at 3 in |- *; rewrite double_var; ring.
+  unfold Rminus in |- *.
+  rewrite <- Ropp_mult_distr_l_reverse.
+  apply Rplus_comm.
+  unfold Rminus in |- *.
+  rewrite <- Ropp_mult_distr_l_reverse.
+  apply Rplus_comm.
+Qed.
+
+Lemma cos_decreasing_0 :
+  forall x y:R,
+    0 <= x -> x <= PI -> 0 <= y -> y <= PI -> cos x < cos y -> y < x.
+Proof.
+  intros; generalize (Ropp_lt_gt_contravar (cos x) (cos y) H3);
+    repeat rewrite <- neg_cos; intro H4;
+      change (cos (y + PI) < cos (x + PI)) in H4; rewrite (Rplus_comm x) in H4;
+        rewrite (Rplus_comm y) in H4; generalize (Rplus_le_compat_l PI 0 x H);
+          generalize (Rplus_le_compat_l PI x PI H0);
+            generalize (Rplus_le_compat_l PI 0 y H1);
+              generalize (Rplus_le_compat_l PI y PI H2); rewrite Rplus_0_r.
+  rewrite <- double.
+  clear H H0 H1 H2 H3; intros; apply Rplus_lt_reg_r with PI;
+    apply (cos_increasing_0 (PI + y) (PI + x) H0 H H2 H1 H4).
+Qed.
+
+Lemma cos_decreasing_1 :
+  forall x y:R,
+    0 <= x -> x <= PI -> 0 <= y -> y <= PI -> x < y -> cos y < cos x.
+Proof.
+  intros; apply Ropp_lt_cancel; repeat rewrite <- neg_cos;
+    rewrite (Rplus_comm x); rewrite (Rplus_comm y);
+      generalize (Rplus_le_compat_l PI 0 x H);
+        generalize (Rplus_le_compat_l PI x PI H0);
+          generalize (Rplus_le_compat_l PI 0 y H1);
+            generalize (Rplus_le_compat_l PI y PI H2); rewrite Rplus_0_r.
+  rewrite <- double.
+  generalize (Rplus_lt_compat_l PI x y H3); clear H H0 H1 H2 H3; intros;
+    apply (cos_increasing_1 (PI + x) (PI + y) H3 H2 H1 H0 H).
+Qed.
+
+Lemma tan_diff :
+  forall x y:R,
+    cos x <> 0 -> cos y <> 0 -> tan x - tan y = sin (x - y) / (cos x * cos y).
+Proof.
+  intros; unfold tan in |- *; rewrite sin_minus.
+  unfold Rdiv in |- *.
+  unfold Rminus in |- *.
+  rewrite Rmult_plus_distr_r.
+  rewrite Rinv_mult_distr.
+  repeat rewrite (Rmult_comm (sin x)).
+  repeat rewrite Rmult_assoc.
+  rewrite (Rmult_comm (cos y)).
+  repeat rewrite Rmult_assoc.
+  rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_r.
+  rewrite (Rmult_comm (sin x)).
+  apply Rplus_eq_compat_l.
+  rewrite <- Ropp_mult_distr_l_reverse.
+  rewrite <- Ropp_mult_distr_r_reverse.
+  rewrite (Rmult_comm (/ cos x)).
+  repeat rewrite Rmult_assoc.
+  rewrite (Rmult_comm (cos x)).
+  repeat rewrite Rmult_assoc.
+  rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_r.
+  reflexivity.
+  assumption.
+  assumption.
+  assumption.
+  assumption.
+Qed.
+
+Lemma tan_increasing_0 :
+  forall x y:R,
+    - (PI / 4) <= x ->
+    x <= PI / 4 -> - (PI / 4) <= y -> y <= PI / 4 -> tan x < tan y -> x < y.
+Proof.
+  intros; generalize PI4_RLT_PI2; intro H4;
+    generalize (Ropp_lt_gt_contravar (PI / 4) (PI / 2) H4);
+      intro H5; change (- (PI / 2) < - (PI / 4)) in H5;
+        generalize
+          (cos_gt_0 x (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) x H5 H)
+            (Rle_lt_trans x (PI / 4) (PI / 2) H0 H4)); intro HP1;
+          generalize
+            (cos_gt_0 y (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) y H5 H1)
+              (Rle_lt_trans y (PI / 4) (PI / 2) H2 H4)); intro HP2;
+            generalize
+              (sym_not_eq
+                (Rlt_not_eq 0 (cos x)
+                  (cos_gt_0 x (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) x H5 H)
+                    (Rle_lt_trans x (PI / 4) (PI / 2) H0 H4))));
+              intro H6;
+                generalize
+                  (sym_not_eq
+                    (Rlt_not_eq 0 (cos y)
+                      (cos_gt_0 y (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) y H5 H1)
+                        (Rle_lt_trans y (PI / 4) (PI / 2) H2 H4))));
+                  intro H7; generalize (tan_diff x y H6 H7); intro H8;
+                    generalize (Rlt_minus (tan x) (tan y) H3); clear H3;
+                      intro H3; rewrite H8 in H3; cut (sin (x - y) < 0).
+  intro H9; generalize (Ropp_le_ge_contravar (- (PI / 4)) y H1);
+    rewrite Ropp_involutive; intro H10; generalize (Rge_le (PI / 4) (- y) H10);
+      clear H10; intro H10; generalize (Ropp_le_ge_contravar y (PI / 4) H2);
+        intro H11; generalize (Rge_le (- y) (- (PI / 4)) H11);
+          clear H11; intro H11;
+            generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11);
+              generalize (Rplus_le_compat x (PI / 4) (- y) (PI / 4) H0 H10);
+                replace (x + - y) with (x - y).
+  replace (PI / 4 + PI / 4) with (PI / 2).
+  replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)).
+  intros; case (Rtotal_order 0 (x - y)); intro H14.
+  generalize
+    (sin_gt_0 (x - y) H14 (Rle_lt_trans (x - y) (PI / 2) PI H12 PI2_Rlt_PI));
+    intro H15; elim (Rlt_irrefl 0 (Rlt_trans 0 (sin (x - y)) 0 H15 H9)).
+  elim H14; intro H15.
+  rewrite <- H15 in H9; rewrite sin_0 in H9; elim (Rlt_irrefl 0 H9).
+  apply Rminus_lt; assumption.
+  pattern PI at 1 in |- *; rewrite double_var.
+  unfold Rdiv in |- *.
+  rewrite Rmult_plus_distr_r.
+  repeat rewrite Rmult_assoc.
+  rewrite <- Rinv_mult_distr.
+  rewrite Ropp_plus_distr.
+  replace 4 with 4.
+  reflexivity.
+  ring.
+  discrR.
+  discrR.
+  pattern PI at 1 in |- *; rewrite double_var.
+  unfold Rdiv in |- *.
+  rewrite Rmult_plus_distr_r.
+  repeat rewrite Rmult_assoc.
+  rewrite <- Rinv_mult_distr.
+  replace 4 with 4.
+  reflexivity.
+  ring.
+  discrR.
+  discrR.
+  reflexivity.
+  case (Rcase_abs (sin (x - y))); intro H9.
+  assumption.
+  generalize (Rge_le (sin (x - y)) 0 H9); clear H9; intro H9;
+    generalize (Rinv_0_lt_compat (cos x) HP1); intro H10;
+      generalize (Rinv_0_lt_compat (cos y) HP2); intro H11;
+        generalize (Rmult_lt_0_compat (/ cos x) (/ cos y) H10 H11);
+          replace (/ cos x * / cos y) with (/ (cos x * cos y)).
+  intro H12;
+    generalize
+      (Rmult_le_pos (sin (x - y)) (/ (cos x * cos y)) H9
+        (Rlt_le 0 (/ (cos x * cos y)) H12)); intro H13;
+      elim
+        (Rlt_irrefl 0 (Rle_lt_trans 0 (sin (x - y) * / (cos x * cos y)) 0 H13 H3)).
+  rewrite Rinv_mult_distr.
+  reflexivity.
+  assumption.
+  assumption.
+Qed.
+
+Lemma tan_increasing_1 :
+  forall x y:R,
+    - (PI / 4) <= x ->
+    x <= PI / 4 -> - (PI / 4) <= y -> y <= PI / 4 -> x < y -> tan x < tan y.
+Proof.
+  intros; apply Rminus_lt; generalize PI4_RLT_PI2; intro H4;
+    generalize (Ropp_lt_gt_contravar (PI / 4) (PI / 2) H4);
+      intro H5; change (- (PI / 2) < - (PI / 4)) in H5;
+        generalize
+          (cos_gt_0 x (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) x H5 H)
+            (Rle_lt_trans x (PI / 4) (PI / 2) H0 H4)); intro HP1;
+          generalize
+            (cos_gt_0 y (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) y H5 H1)
+              (Rle_lt_trans y (PI / 4) (PI / 2) H2 H4)); intro HP2;
+            generalize
+              (sym_not_eq
+                (Rlt_not_eq 0 (cos x)
+                  (cos_gt_0 x (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) x H5 H)
+                    (Rle_lt_trans x (PI / 4) (PI / 2) H0 H4))));
+              intro H6;
+                generalize
+                  (sym_not_eq
+                    (Rlt_not_eq 0 (cos y)
+                      (cos_gt_0 y (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) y H5 H1)
+                        (Rle_lt_trans y (PI / 4) (PI / 2) H2 H4))));
+                  intro H7; rewrite (tan_diff x y H6 H7);
+                    generalize (Rinv_0_lt_compat (cos x) HP1); intro H10;
+                      generalize (Rinv_0_lt_compat (cos y) HP2); intro H11;
+                        generalize (Rmult_lt_0_compat (/ cos x) (/ cos y) H10 H11);
+                          replace (/ cos x * / cos y) with (/ (cos x * cos y)).
+  clear H10 H11; intro H8; generalize (Ropp_le_ge_contravar y (PI / 4) H2);
+    intro H11; generalize (Rge_le (- y) (- (PI / 4)) H11);
+      clear H11; intro H11;
+        generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11);
+          replace (x + - y) with (x - y).
+  replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)).
+  clear H11; intro H9; generalize (Rlt_minus x y H3); clear H3; intro H3;
+    clear H H0 H1 H2 H4 H5 HP1 HP2; generalize PI2_Rlt_PI;
+      intro H1; generalize (Ropp_lt_gt_contravar (PI / 2) PI H1);
+        clear H1; intro H1;
+          generalize
+            (sin_lt_0_var (x - y) (Rlt_le_trans (- PI) (- (PI / 2)) (x - y) H1 H9) H3);
+            intro H2;
+              generalize
+                (Rmult_lt_gt_compat_neg_l (sin (x - y)) 0 (/ (cos x * cos y)) H2 H8);
+                rewrite Rmult_0_r; intro H4; assumption.
+  pattern PI at 1 in |- *; rewrite double_var.
+  unfold Rdiv in |- *.
+  rewrite Rmult_plus_distr_r.
+  repeat rewrite Rmult_assoc.
+  rewrite <- Rinv_mult_distr.
+  replace 4 with 4.
+  rewrite Ropp_plus_distr.
+  reflexivity.
+  ring.
+  discrR.
+  discrR.
+  reflexivity.
+  apply Rinv_mult_distr; assumption.
+Qed.
+
+Lemma sin_incr_0 :
+  forall x y:R,
+    - (PI / 2) <= x ->
+    x <= PI / 2 -> - (PI / 2) <= y -> y <= PI / 2 -> sin x <= sin y -> x <= y.
+Proof.
+  intros; case (Rtotal_order (sin x) (sin y)); intro H4;
+    [ left; apply (sin_increasing_0 x y H H0 H1 H2 H4)
+      | elim H4; intro H5;
+        [ case (Rtotal_order x y); intro H6;
+          [ left; assumption
+            | elim H6; intro H7;
+              [ right; assumption
+                | generalize (sin_increasing_1 y x H1 H2 H H0 H7); intro H8;
+                  rewrite H5 in H8; elim (Rlt_irrefl (sin y) H8) ] ]
+          | elim (Rlt_irrefl (sin x) (Rle_lt_trans (sin x) (sin y) (sin x) H3 H5)) ] ].
+Qed.
+
+Lemma sin_incr_1 :
+  forall x y:R,
+    - (PI / 2) <= x ->
+    x <= PI / 2 -> - (PI / 2) <= y -> y <= PI / 2 -> x <= y -> sin x <= sin y.
+Proof.
+  intros; case (Rtotal_order x y); intro H4;
+    [ left; apply (sin_increasing_1 x y H H0 H1 H2 H4)
+      | elim H4; intro H5;
+        [ case (Rtotal_order (sin x) (sin y)); intro H6;
+          [ left; assumption
+            | elim H6; intro H7;
+              [ right; assumption
+                | generalize (sin_increasing_0 y x H1 H2 H H0 H7); intro H8;
+                  rewrite H5 in H8; elim (Rlt_irrefl y H8) ] ]
+          | elim (Rlt_irrefl x (Rle_lt_trans x y x H3 H5)) ] ].
+Qed.
+
+Lemma sin_decr_0 :
+  forall x y:R,
+    x <= 3 * (PI / 2) ->
+    PI / 2 <= x ->
+    y <= 3 * (PI / 2) -> PI / 2 <= y -> sin x <= sin y -> y <= x.
+Proof.
+  intros; case (Rtotal_order (sin x) (sin y)); intro H4;
+    [ left; apply (sin_decreasing_0 x y H H0 H1 H2 H4)
+      | elim H4; intro H5;
+        [ case (Rtotal_order x y); intro H6;
+          [ generalize (sin_decreasing_1 x y H H0 H1 H2 H6); intro H8;
+            rewrite H5 in H8; elim (Rlt_irrefl (sin y) H8)
+            | elim H6; intro H7;
+              [ right; symmetry  in |- *; assumption | left; assumption ] ]
+          | elim (Rlt_irrefl (sin x) (Rle_lt_trans (sin x) (sin y) (sin x) H3 H5)) ] ].
+Qed.
+
+Lemma sin_decr_1 :
+  forall x y:R,
+    x <= 3 * (PI / 2) ->
+    PI / 2 <= x ->
+    y <= 3 * (PI / 2) -> PI / 2 <= y -> x <= y -> sin y <= sin x.
+Proof.
+  intros; case (Rtotal_order x y); intro H4;
+    [ left; apply (sin_decreasing_1 x y H H0 H1 H2 H4)
+      | elim H4; intro H5;
+        [ case (Rtotal_order (sin x) (sin y)); intro H6;
+          [ generalize (sin_decreasing_0 x y H H0 H1 H2 H6); intro H8;
+            rewrite H5 in H8; elim (Rlt_irrefl y H8)
+            | elim H6; intro H7;
+              [ right; symmetry  in |- *; assumption | left; assumption ] ]
+          | elim (Rlt_irrefl x (Rle_lt_trans x y x H3 H5)) ] ].
+Qed.
+
+Lemma cos_incr_0 :
+  forall x y:R,
+    PI <= x ->
+    x <= 2 * PI -> PI <= y -> y <= 2 * PI -> cos x <= cos y -> x <= y.
+Proof.
+  intros; case (Rtotal_order (cos x) (cos y)); intro H4;
+    [ left; apply (cos_increasing_0 x y H H0 H1 H2 H4)
+      | elim H4; intro H5;
+        [ case (Rtotal_order x y); intro H6;
+          [ left; assumption
+            | elim H6; intro H7;
+              [ right; assumption
+                | generalize (cos_increasing_1 y x H1 H2 H H0 H7); intro H8;
+                  rewrite H5 in H8; elim (Rlt_irrefl (cos y) H8) ] ]
+          | elim (Rlt_irrefl (cos x) (Rle_lt_trans (cos x) (cos y) (cos x) H3 H5)) ] ].
+Qed.
+
+Lemma cos_incr_1 :
+  forall x y:R,
+    PI <= x ->
+    x <= 2 * PI -> PI <= y -> y <= 2 * PI -> x <= y -> cos x <= cos y.
+Proof.
+  intros; case (Rtotal_order x y); intro H4;
+    [ left; apply (cos_increasing_1 x y H H0 H1 H2 H4)
+      | elim H4; intro H5;
+        [ case (Rtotal_order (cos x) (cos y)); intro H6;
+          [ left; assumption
+            | elim H6; intro H7;
+              [ right; assumption
+                | generalize (cos_increasing_0 y x H1 H2 H H0 H7); intro H8;
+                  rewrite H5 in H8; elim (Rlt_irrefl y H8) ] ]
+          | elim (Rlt_irrefl x (Rle_lt_trans x y x H3 H5)) ] ].
+Qed.
+
+Lemma cos_decr_0 :
+  forall x y:R,
+    0 <= x -> x <= PI -> 0 <= y -> y <= PI -> cos x <= cos y -> y <= x.
+Proof.
+  intros; case (Rtotal_order (cos x) (cos y)); intro H4;
+    [ left; apply (cos_decreasing_0 x y H H0 H1 H2 H4)
+      | elim H4; intro H5;
+        [ case (Rtotal_order x y); intro H6;
+          [ generalize (cos_decreasing_1 x y H H0 H1 H2 H6); intro H8;
+            rewrite H5 in H8; elim (Rlt_irrefl (cos y) H8)
+            | elim H6; intro H7;
+              [ right; symmetry  in |- *; assumption | left; assumption ] ]
+          | elim (Rlt_irrefl (cos x) (Rle_lt_trans (cos x) (cos y) (cos x) H3 H5)) ] ].
+Qed.
+
+Lemma cos_decr_1 :
+  forall x y:R,
+    0 <= x -> x <= PI -> 0 <= y -> y <= PI -> x <= y -> cos y <= cos x.
+Proof.
+  intros; case (Rtotal_order x y); intro H4;
+    [ left; apply (cos_decreasing_1 x y H H0 H1 H2 H4)
+      | elim H4; intro H5;
+        [ case (Rtotal_order (cos x) (cos y)); intro H6;
+          [ generalize (cos_decreasing_0 x y H H0 H1 H2 H6); intro H8;
+            rewrite H5 in H8; elim (Rlt_irrefl y H8)
+            | elim H6; intro H7;
+              [ right; symmetry  in |- *; assumption | left; assumption ] ]
+          | elim (Rlt_irrefl x (Rle_lt_trans x y x H3 H5)) ] ].
+Qed.
+
+Lemma tan_incr_0 :
+  forall x y:R,
+    - (PI / 4) <= x ->
+    x <= PI / 4 -> - (PI / 4) <= y -> y <= PI / 4 -> tan x <= tan y -> x <= y.
+Proof.
+  intros; case (Rtotal_order (tan x) (tan y)); intro H4;
+    [ left; apply (tan_increasing_0 x y H H0 H1 H2 H4)
+      | elim H4; intro H5;
+        [ case (Rtotal_order x y); intro H6;
+          [ left; assumption
+            | elim H6; intro H7;
+              [ right; assumption
+                | generalize (tan_increasing_1 y x H1 H2 H H0 H7); intro H8;
+                  rewrite H5 in H8; elim (Rlt_irrefl (tan y) H8) ] ]
+          | elim (Rlt_irrefl (tan x) (Rle_lt_trans (tan x) (tan y) (tan x) H3 H5)) ] ].
+Qed.
+
+Lemma tan_incr_1 :
+  forall x y:R,
+    - (PI / 4) <= x ->
+    x <= PI / 4 -> - (PI / 4) <= y -> y <= PI / 4 -> x <= y -> tan x <= tan y.
+Proof.
+  intros; case (Rtotal_order x y); intro H4;
+    [ left; apply (tan_increasing_1 x y H H0 H1 H2 H4)
+      | elim H4; intro H5;
+        [ case (Rtotal_order (tan x) (tan y)); intro H6;
+          [ left; assumption
+            | elim H6; intro H7;
+              [ right; assumption
+                | generalize (tan_increasing_0 y x H1 H2 H H0 H7); intro H8;
+                  rewrite H5 in H8; elim (Rlt_irrefl y H8) ] ]
+          | elim (Rlt_irrefl x (Rle_lt_trans x y x H3 H5)) ] ].
+Qed.
+
+(**********)
+Lemma sin_eq_0_1 : forall x:R, (exists k : Z, x = IZR k * PI) -> sin x = 0.
+Proof.
+  intros.
+  elim H; intros.
+  apply (Zcase_sign x0).
+  intro.
+  rewrite H1 in H0.
+  simpl in H0.
+  rewrite H0; rewrite Rmult_0_l; apply sin_0.
+  intro.
+  cut (0 <= x0)%Z.
+  intro.
+  elim (IZN x0 H2); intros.
+  rewrite H3 in H0.
+  rewrite <- INR_IZR_INZ in H0.
+  rewrite H0.
+  elim (even_odd_cor x1); intros.
+  elim H4; intro.
+  rewrite H5.
+  rewrite mult_INR.
+  simpl in |- *.
+  rewrite <- (Rplus_0_l (2 * INR x2 * PI)).
+  rewrite sin_period.
+  apply sin_0.
+  rewrite H5.
+  rewrite S_INR; rewrite mult_INR.
+  simpl in |- *.
+  rewrite Rmult_plus_distr_r.
+  rewrite Rmult_1_l; rewrite sin_plus.
+  rewrite sin_PI.
+  rewrite Rmult_0_r.
+  rewrite <- (Rplus_0_l (2 * INR x2 * PI)).
+  rewrite sin_period.
+  rewrite sin_0; ring.
+  apply le_IZR.
+  left; apply IZR_lt.
+  assert (H2 := Zorder.Zgt_iff_lt).
+  elim (H2 x0 0%Z); intros.
+  apply H3; assumption.
+  intro.
+  rewrite H0.
+  replace (sin (IZR x0 * PI)) with (- sin (- IZR x0 * PI)).
+  cut (0 <= - x0)%Z.
+  intro.
+  rewrite <- Ropp_Ropp_IZR.
+  elim (IZN (- x0) H2); intros.
+  rewrite H3.
+  rewrite <- INR_IZR_INZ.
+  elim (even_odd_cor x1); intros.
+  elim H4; intro.
+  rewrite H5.
+  rewrite mult_INR.
+  simpl in |- *.
+  rewrite <- (Rplus_0_l (2 * INR x2 * PI)).
+  rewrite sin_period.
+  rewrite sin_0; ring.
+  rewrite H5.
+  rewrite S_INR; rewrite mult_INR.
+  simpl in |- *.
+  rewrite Rmult_plus_distr_r.
+  rewrite Rmult_1_l; rewrite sin_plus.
+  rewrite sin_PI.
+  rewrite Rmult_0_r.
+  rewrite <- (Rplus_0_l (2 * INR x2 * PI)).
+  rewrite sin_period.
+  rewrite sin_0; ring.
+  apply le_IZR.
+  apply Rplus_le_reg_l with (IZR x0).
+  rewrite Rplus_0_r.
+  rewrite Ropp_Ropp_IZR.
+  rewrite Rplus_opp_r.
+  left; replace 0 with (IZR 0); [ apply IZR_lt | reflexivity ].
+  assumption.
+  rewrite <- sin_neg.
+  rewrite Ropp_mult_distr_l_reverse.
+  rewrite Ropp_involutive.
+  reflexivity.
+Qed.
+
+Lemma sin_eq_0_0 : forall x:R, sin x = 0 ->  exists k : Z, x = IZR k * PI.
+Proof.
+  intros.
+  assert (H0 := euclidian_division x PI PI_neq0).
+  elim H0; intros q H1.
+  elim H1; intros r H2.
+  exists q.
+  cut (r = 0).
+  intro.
+  elim H2; intros H4 _; rewrite H4; rewrite H3.
+  apply Rplus_0_r.
+  elim H2; intros.
+  rewrite H3 in H.
+  rewrite sin_plus in H.
+  cut (sin (IZR q * PI) = 0).
+  intro.
+  rewrite H5 in H.
+  rewrite Rmult_0_l in H.
+  rewrite Rplus_0_l in H.
+  assert (H6 := Rmult_integral _ _ H).
+  elim H6; intro.
+  assert (H8 := sin2_cos2 (IZR q * PI)).
+  rewrite H5 in H8; rewrite H7 in H8.
+  rewrite Rsqr_0 in H8.
+  rewrite Rplus_0_r in H8.
+  elim R1_neq_R0; symmetry  in |- *; assumption.
+  cut (r = 0 \/ 0 < r < PI).
+  intro; elim H8; intro.
+  assumption.
+  elim H9; intros.
+  assert (H12 := sin_gt_0 _ H10 H11).
+  rewrite H7 in H12; elim (Rlt_irrefl _ H12).
+  rewrite Rabs_right in H4.
+  elim H4; intros.
+  case (Rtotal_order 0 r); intro.
+  right; split; assumption.
+  elim H10; intro.
+  left; symmetry  in |- *; assumption.
+  elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H8 H11)).
+  apply Rle_ge.
+  left; apply PI_RGT_0.
+  apply sin_eq_0_1.
+  exists q; reflexivity.
+Qed.
+
+Lemma cos_eq_0_0 :
+  forall x:R, cos x = 0 ->  exists k : Z, x = IZR k * PI + PI / 2.
+Proof.
+  intros x H; rewrite cos_sin in H; generalize (sin_eq_0_0 (PI / INR 2 + x) H);
+    intro H2; elim H2; intros x0 H3; exists (x0 - Z_of_nat 1)%Z;
+      rewrite <- Z_R_minus; simpl.
+unfold INR in H3. field_simplify [(sym_eq H3)]. field.
+(**
+  ring_simplify.
+ (* rewrite (Rmult_comm PI);*) (* old ring compat *)
+        rewrite <- H3; simpl;
+          field;repeat split; discrR.
+*)
+Qed.
+
+Lemma cos_eq_0_1 :
+  forall x:R, (exists k : Z, x = IZR k * PI + PI / 2) -> cos x = 0.
+Proof.
+  intros x H1; rewrite cos_sin; elim H1; intros x0 H2; rewrite H2;
+    replace (PI / 2 + (IZR x0 * PI + PI / 2)) with (IZR x0 * PI + PI).
+  rewrite neg_sin; rewrite <- Ropp_0.
+  apply Ropp_eq_compat; apply sin_eq_0_1; exists x0; reflexivity.
+  pattern PI at 2 in |- *; rewrite (double_var PI); ring.
+Qed.
+
+Lemma sin_eq_O_2PI_0 :
+  forall x:R,
+    0 <= x -> x <= 2 * PI -> sin x = 0 -> x = 0 \/ x = PI \/ x = 2 * PI.
+Proof.
+  intros; generalize (sin_eq_0_0 x H1); intro.
+  elim H2; intros k0 H3.
+  case (Rtotal_order PI x); intro.
+  rewrite H3 in H4; rewrite H3 in H0.
+  right; right.
+  generalize
+    (Rmult_lt_compat_r (/ PI) PI (IZR k0 * PI) (Rinv_0_lt_compat PI PI_RGT_0) H4);
+    rewrite Rmult_assoc; repeat rewrite <- Rinv_r_sym.
+  rewrite Rmult_1_r; intro;
+    generalize
+      (Rmult_le_compat_r (/ PI) (IZR k0 * PI) (2 * PI)
+        (Rlt_le 0 (/ PI) (Rinv_0_lt_compat PI PI_RGT_0)) H0);
+      repeat rewrite Rmult_assoc; repeat rewrite <- Rinv_r_sym.
+  repeat rewrite Rmult_1_r; intro;
+    generalize (Rplus_lt_compat_l (IZR (-2)) 1 (IZR k0) H5);
+      rewrite <- plus_IZR.
+  replace (IZR (-2) + 1) with (-1).
+  intro; generalize (Rplus_le_compat_l (IZR (-2)) (IZR k0) 2 H6);
+    rewrite <- plus_IZR.
+  replace (IZR (-2) + 2) with 0.
+  intro; cut (-1 < IZR (-2 + k0) < 1).
+  intro; generalize (one_IZR_lt1 (-2 + k0) H9); intro.
+  cut (k0 = 2%Z).
+  intro; rewrite H11 in H3; rewrite H3; simpl in |- *.
+  reflexivity.
+  rewrite <- (Zplus_opp_l 2) in H10; generalize (Zplus_reg_l (-2) k0 2 H10);
+    intro; assumption.
+  split.
+  assumption.
+  apply Rle_lt_trans with 0.
+  assumption.
+  apply Rlt_0_1.
+  simpl in |- *; ring.
+  simpl in |- *; ring.
+  apply PI_neq0.
+  apply PI_neq0.
+  elim H4; intro.
+  right; left.
+  symmetry  in |- *; assumption.
+  left.
+  rewrite H3 in H5; rewrite H3 in H;
+    generalize
+      (Rmult_lt_compat_r (/ PI) (IZR k0 * PI) PI (Rinv_0_lt_compat PI PI_RGT_0)
+        H5); rewrite Rmult_assoc; repeat rewrite <- Rinv_r_sym.
+  rewrite Rmult_1_r; intro;
+    generalize
+      (Rmult_le_compat_r (/ PI) 0 (IZR k0 * PI)
+        (Rlt_le 0 (/ PI) (Rinv_0_lt_compat PI PI_RGT_0)) H);
+      repeat rewrite Rmult_assoc; repeat rewrite <- Rinv_r_sym.
+  rewrite Rmult_1_r; rewrite Rmult_0_l; intro.
+  cut (-1 < IZR k0 < 1).
+  intro; generalize (one_IZR_lt1 k0 H8); intro; rewrite H9 in H3; rewrite H3;
+    simpl in |- *; apply Rmult_0_l.
+  split.
+  apply Rlt_le_trans with 0.
+  rewrite <- Ropp_0; apply Ropp_gt_lt_contravar; apply Rlt_0_1.
+  assumption.
+  assumption.
+  apply PI_neq0.
+  apply PI_neq0.
+Qed.
+
+Lemma sin_eq_O_2PI_1 :
+  forall x:R,
+    0 <= x -> x <= 2 * PI -> x = 0 \/ x = PI \/ x = 2 * PI -> sin x = 0.
+Proof.
+  intros x H1 H2 H3; elim H3; intro H4;
+    [ rewrite H4; rewrite sin_0; reflexivity
+      | elim H4; intro H5;
+        [ rewrite H5; rewrite sin_PI; reflexivity
+          | rewrite H5; rewrite sin_2PI; reflexivity ] ].
+Qed.
+
+Lemma cos_eq_0_2PI_0 :
+  forall x:R,
+    0 <= x -> x <= 2 * PI -> cos x = 0 -> x = PI / 2 \/ x = 3 * (PI / 2).
+Proof.
+  intros; case (Rtotal_order x (3 * (PI / 2))); intro.
+  rewrite cos_sin in H1.
+  cut (0 <= PI / 2 + x).
+  cut (PI / 2 + x <= 2 * PI).
+  intros; generalize (sin_eq_O_2PI_0 (PI / 2 + x) H4 H3 H1); intros.
+  decompose [or] H5.
+  generalize (Rplus_le_compat_l (PI / 2) 0 x H); rewrite Rplus_0_r; rewrite H6;
+    intro.
+  elim (Rlt_irrefl 0 (Rlt_le_trans 0 (PI / 2) 0 PI2_RGT_0 H7)).
+  left.
+  generalize (Rplus_eq_compat_l (- (PI / 2)) (PI / 2 + x) PI H7).
+  replace (- (PI / 2) + (PI / 2 + x)) with x.
+  replace (- (PI / 2) + PI) with (PI / 2).
+  intro; assumption.
+  pattern PI at 3 in |- *; rewrite (double_var PI); ring.
+  ring.
+  right.
+  generalize (Rplus_eq_compat_l (- (PI / 2)) (PI / 2 + x) (2 * PI) H7).
+  replace (- (PI / 2) + (PI / 2 + x)) with x.
+  replace (- (PI / 2) + 2 * PI) with (3 * (PI / 2)).
+  intro; assumption.
+  rewrite double; pattern PI at 3 4 in |- *; rewrite (double_var PI); ring.
+  ring.
+  left; replace (2 * PI) with (PI / 2 + 3 * (PI / 2)).
+  apply Rplus_lt_compat_l; assumption.
+  rewrite (double PI); pattern PI at 3 4 in |- *; rewrite (double_var PI); ring.
+  apply Rplus_le_le_0_compat.
+  left; unfold Rdiv in |- *; apply Rmult_lt_0_compat.
+  apply PI_RGT_0.
+  apply Rinv_0_lt_compat; prove_sup0.
+  assumption.
+  elim H2; intro.
+  right; assumption.
+  generalize (cos_eq_0_0 x H1); intro; elim H4; intros k0 H5.
+  rewrite H5 in H3; rewrite H5 in H0;
+    generalize
+      (Rplus_lt_compat_l (- (PI / 2)) (3 * (PI / 2)) (IZR k0 * PI + PI / 2) H3);
+      generalize
+        (Rplus_le_compat_l (- (PI / 2)) (IZR k0 * PI + PI / 2) (2 * PI) H0).
+  replace (- (PI / 2) + 3 * (PI / 2)) with PI.
+  replace (- (PI / 2) + (IZR k0 * PI + PI / 2)) with (IZR k0 * PI).
+  replace (- (PI / 2) + 2 * PI) with (3 * (PI / 2)).
+  intros;
+    generalize
+      (Rmult_lt_compat_l (/ PI) PI (IZR k0 * PI) (Rinv_0_lt_compat PI PI_RGT_0)
+        H7);
+      generalize
+        (Rmult_le_compat_l (/ PI) (IZR k0 * PI) (3 * (PI / 2))
+          (Rlt_le 0 (/ PI) (Rinv_0_lt_compat PI PI_RGT_0)) H6).
+  replace (/ PI * (IZR k0 * PI)) with (IZR k0).
+  replace (/ PI * (3 * (PI / 2))) with (3 * / 2).
+  rewrite <- Rinv_l_sym.
+  intros; generalize (Rplus_lt_compat_l (IZR (-2)) 1 (IZR k0) H9);
+    rewrite <- plus_IZR.
+  replace (IZR (-2) + 1) with (-1).
+  intro; generalize (Rplus_le_compat_l (IZR (-2)) (IZR k0) (3 * / 2) H8);
+    rewrite <- plus_IZR.
+  replace (IZR (-2) + 2) with 0.
+  intro; cut (-1 < IZR (-2 + k0) < 1).
+  intro; generalize (one_IZR_lt1 (-2 + k0) H12); intro.
+  cut (k0 = 2%Z).
+  intro; rewrite H14 in H8.
+  assert (Hyp : 0 < 2).
+  prove_sup0.
+  generalize (Rmult_le_compat_l 2 (IZR 2) (3 * / 2) (Rlt_le 0 2 Hyp) H8);
+    simpl in |- *.
+  replace 4 with 4.
+  replace (2 * (3 * / 2)) with 3.
+  intro; cut (3 < 4).
+  intro; elim (Rlt_irrefl 3 (Rlt_le_trans 3 4 3 H16 H15)).
+  generalize (Rplus_lt_compat_l 3 0 1 Rlt_0_1); rewrite Rplus_0_r.
+  replace (3 + 1) with 4.
+  intro; assumption.
+  ring.
+  symmetry  in |- *; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m.
+  discrR.
+  ring.
+  rewrite <- (Zplus_opp_l 2) in H13; generalize (Zplus_reg_l (-2) k0 2 H13);
+    intro; assumption.
+  split.
+  assumption.
+  apply Rle_lt_trans with (IZR (-2) + 3 * / 2).
+  assumption.
+  simpl in |- *; replace (-2 + 3 * / 2) with (- (1 * / 2)).
+  apply Rlt_trans with 0.
+  rewrite <- Ropp_0; apply Ropp_lt_gt_contravar.
+  apply Rmult_lt_0_compat;
+    [ apply Rlt_0_1 | apply Rinv_0_lt_compat; prove_sup0 ].
+  apply Rlt_0_1.
+  rewrite Rmult_1_l; apply Rmult_eq_reg_l with 2.
+  rewrite Ropp_mult_distr_r_reverse; rewrite <- Rinv_r_sym.
+  rewrite Rmult_plus_distr_l; rewrite <- Rmult_assoc; rewrite Rinv_r_simpl_m.
+  ring.
+  discrR.
+  discrR.
+  discrR.
+  simpl in |- *; ring.
+  simpl in |- *; ring.
+  apply PI_neq0.
+  unfold Rdiv in |- *; pattern 3 at 1 in |- *; rewrite (Rmult_comm 3);
+    repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_l; apply Rmult_comm.
+  apply PI_neq0.
+  symmetry  in |- *; rewrite (Rmult_comm (/ PI)); rewrite Rmult_assoc;
+    rewrite <- Rinv_r_sym.
+  apply Rmult_1_r.
+  apply PI_neq0.
+  rewrite double; pattern PI at 3 4 in |- *; rewrite double_var; ring.
+  ring.
+  pattern PI at 1 in |- *; rewrite double_var; ring.
+Qed.
+
+Lemma cos_eq_0_2PI_1 :
+  forall x:R,
+    0 <= x -> x <= 2 * PI -> x = PI / 2 \/ x = 3 * (PI / 2) -> cos x = 0.
+Proof.
+  intros x H1 H2 H3; elim H3; intro H4;
+    [ rewrite H4; rewrite cos_PI2; reflexivity
+      | rewrite H4; rewrite cos_3PI2; reflexivity ].
+Qed.