Merge PR #7897: Remove fourier plugin

35 files changed, 314 insertions, 1411 deletions

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index bbd2d349c..d3b347862 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -135,9 +135,6 @@
 /plugins/firstorder/   @PierreCorbineau
 # Secondary maintainer @herbelin
 
-/plugins/fourier/       @herbelin
-# Secondary maintainer @gares
-
 /plugins/funind/        @forestjulien
 # Secondary maintainer @Matafou
 
diff --git a/CHANGES b/CHANGES
index fdd4feb59..2df231f26 100644
--- a/CHANGES
+++ b/CHANGES
@@ -39,6 +39,9 @@ Tactics
   still be used if you really want to ignore universe constraints.
 
 - Tactics and tactic notations now understand the `deprecated` attribute.
+- The `fourier` tactic has been removed. Please now use `lra` instead. You
+  may need to add `Require Import Lra` to your developments. For compatibility,
+  we now define `fourier` as a deprecated alias of `lra`.
 
 Tools
 
diff --git a/CREDITS b/CREDITS
index f59bfca86..9c3a93da8 100644
--- a/CREDITS
+++ b/CREDITS
@@ -37,8 +37,6 @@ plugins/extraction
   developed by Pierre Letouzey (LRI, 2000-2004, PPS, 2005-now)
 plugins/firstorder
   developed by Pierre Corbineau (LRI, 2003-2008)
-plugins/fourier
-  developed by Loïc Pottier (INRIA-Lemme, 2001)
 plugins/funind
   developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2006-now),
   Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008, ENSIIE, 2008-now)
diff --git a/META.coq b/META.coq
index a7c8da163..b2924e324 100644
--- a/META.coq
+++ b/META.coq
@@ -349,18 +349,6 @@ package "plugins" (
     archive(native)  = "newring_plugin.cmx"
   )
 
-  package "fourier" (
-
-    description = "Coq fourier plugin"
-    version     = "8.9"
-
-    requires    = "coq.plugins.ltac"
-    directory   = "fourier"
-
-    archive(byte)    = "fourier_plugin.cmo"
-    archive(native)  = "fourier_plugin.cmx"
-  )
-
   package "extraction" (
 
     description = "Coq extraction plugin"
diff --git a/Makefile.common b/Makefile.common
index 727cb1e69..772561bd7 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -96,7 +96,7 @@ CORESRCDIRS:=\
 
 PLUGINDIRS:=\
   omega		romega 		micromega 	quote \
-  setoid_ring 	extraction 	fourier \
+  setoid_ring 	extraction \
   cc 		funind 		firstorder 	derive \
   rtauto 	nsatz           syntax          btauto \
   ssrmatching	ltac		ssr
@@ -134,7 +134,6 @@ MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo
 QUOTECMO:=plugins/quote/quote_plugin.cmo
 RINGCMO:=plugins/setoid_ring/newring_plugin.cmo
 NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo
-FOURIERCMO:=plugins/fourier/fourier_plugin.cmo
 EXTRACTIONCMO:=plugins/extraction/extraction_plugin.cmo
 FUNINDCMO:=plugins/funind/recdef_plugin.cmo
 FOCMO:=plugins/firstorder/ground_plugin.cmo
@@ -155,7 +154,7 @@ SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
 
 PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
         $(QUOTECMO) $(RINGCMO) \
-        $(FOURIERCMO) $(EXTRACTIONCMO) \
+        $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
         $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \
 	$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO)
diff --git a/Makefile.dev b/Makefile.dev
index 8f7d21694..7fc1076a8 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -174,7 +174,6 @@ MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO))
 QUOTEVO:=$(filter plugins/quote/%, $(PLUGINSVO))
 RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO))
 NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO))
-FOURIERVO:=$(filter plugins/fourier/%, $(PLUGINSVO))
 FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO))
 BTAUTOVO:=$(filter plugins/btauto/%, $(PLUGINSVO))
 RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO))
@@ -188,7 +187,6 @@ micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
 setoid_ring: $(RINGVO) $(RINGCMO)
 nsatz: $(NSATZVO) $(NSATZCMO)
 extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO)
-fourier: $(FOURIERVO) $(FOURIERCMO)
 funind: $(FUNINDCMO) $(FUNINDVO)
 cc: $(CCVO) $(CCCMO)
 rtauto: $(RTAUTOVO) $(RTAUTOCMO)
@@ -196,7 +194,7 @@ btauto: $(BTAUTOVO) $(BTAUTOCMO)
 ltac: $(LTACVO) $(LTACCMO)
 
 .PHONY: omega micromega setoid_ring nsatz extraction
-.PHONY: fourier funind cc rtauto btauto ltac
+.PHONY: funind cc rtauto btauto ltac
 
 # For emacs:
 # Local Variables:
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 2bec09de2..bccd3fefb 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -33,7 +33,7 @@ if [ -z "$GUESS_CHECKER" ]; then
 	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
         -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
         -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
-        -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \
+        -I $COQTOP/plugins/firstorder \
         -I $COQTOP/plugins/funind     -I $COQTOP/plugins/groebner \
         -I $COQTOP/plugins/interface  -I $COQTOP/plugins/micromega \
         -I $COQTOP/plugins/omega      -I $COQTOP/plugins/quote \
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 0e9c23b9b..2407a9051 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -96,15 +96,14 @@ and checked to be :math:`-1`.
 .. tacn:: lra
    :name: lra
 
-This tactic is searching for *linear* refutations using Fourier
-elimination [#]_. As a result, this tactic explores a subset of the *Cone*
-defined as
+   This tactic is searching for *linear* refutations using Fourier
+   elimination [#]_. As a result, this tactic explores a subset of the *Cone*
+   defined as
 
-  :math:`\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}`
+   :math:`\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}`
 
-The deductive power of `lra` is the combined deductive power of
-`ring_simplify` and `fourier`. There is also an overlap with the field
-tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`.
+   The deductive power of :tacn:`lra` overlaps with the one of :tacn:`field`
+   tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`.
 
 
 `lia`: a tactic for linear integer arithmetic
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index afb49413d..f23e04c3a 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -889,7 +889,7 @@ Notation          Interpretation
 Some tactics for real numbers
 +++++++++++++++++++++++++++++
 
-In addition to the powerful ``ring``, ``field`` and ``fourier``
+In addition to the powerful ``ring``, ``field`` and ``lra``
 tactics (see Chapter :ref:`tactics`), there are also:
 
 .. tacn:: discrR
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index ec085a71e..562f8568d 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4319,21 +4319,6 @@ printed with the Print Fields command.
 See also: file plugins/setoid_ring/RealField.v for an example of instantiation,
 theory theories/Reals for many examples of use of field.
 
-.. tacn:: fourier
-   :name: fourier
-
-This tactic written by Loïc Pottier solves linear inequalities on real
-numbers using Fourier’s method :cite:`Fourier`. This tactic must be loaded by
-``Require Import Fourier``.
-
-.. example::
-   .. coqtop:: reset all
-
-      Require Import Reals.
-      Require Import Fourier.
-      Goal forall x y:R, (x < y)%R -> (y + 1 >= x - 1)%R.
-      intros; fourier.
-
 Non-logical tactics
 ------------------------
 
diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map
index 47612cdf7..54a592a04 100644
--- a/ide/MacOS/default_accel_map
+++ b/ide/MacOS/default_accel_map
@@ -217,7 +217,6 @@
 ; (gtk_accel_path "<Actions>/Tactics/Tactic casetype" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic cbv in" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Load" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic fourier" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Goal" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic exists" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic decompose record" "")
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index f5dba2085..b0bafb793 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -311,7 +311,6 @@ let tactics =
      "fix __ with";
      "fold";
      "fold __ in";
-     "fourier";
      "functional induction";
    ];
 
diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v
deleted file mode 100644
index 07f32be8e..000000000
--- a/plugins/fourier/Fourier.v
+++ /dev/null
@@ -1,20 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* "Fourier's method to solve linear inequations/equations systems.".*)
-
-Require Export Field.
-Require Export DiscrR.
-Require Export Fourier_util.
-Declare ML Module "fourier_plugin".
-
-Ltac fourier := abstract (compute [IZR IPR IPR_2] in *; fourierz; field; discrR).
-
-Ltac fourier_eq := apply Rge_antisym; fourier.
diff --git a/plugins/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v
deleted file mode 100644
index d3159698b..000000000
--- a/plugins/fourier/Fourier_util.v
+++ /dev/null
@@ -1,222 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-Require Export Rbase.
-Comments "Lemmas used by the tactic Fourier".
-
-Open Scope R_scope.
-
-Lemma Rfourier_lt : forall x1 y1 a:R, x1 < y1 -> 0 < a -> a * x1 < a * y1.
-intros; apply Rmult_lt_compat_l; assumption.
-Qed.
-
-Lemma Rfourier_le : forall x1 y1 a:R, x1 <= y1 -> 0 < a -> a * x1 <= a * y1.
-red.
-intros.
-case H; auto with real.
-Qed.
-
-Lemma Rfourier_lt_lt :
- forall x1 y1 x2 y2 a:R,
-   x1 < y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2.
-intros x1 y1 x2 y2 a H H0 H1; try assumption.
-apply Rplus_lt_compat.
-try exact H.
-apply Rfourier_lt.
-try exact H0.
-try exact H1.
-Qed.
-
-Lemma Rfourier_lt_le :
- forall x1 y1 x2 y2 a:R,
-   x1 < y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2.
-intros x1 y1 x2 y2 a H H0 H1; try assumption.
-case H0; intros.
-apply Rplus_lt_compat.
-try exact H.
-apply Rfourier_lt; auto with real.
-rewrite H2.
-rewrite (Rplus_comm y1 (a * y2)).
-rewrite (Rplus_comm x1 (a * y2)).
-apply Rplus_lt_compat_l.
-try exact H.
-Qed.
-
-Lemma Rfourier_le_lt :
- forall x1 y1 x2 y2 a:R,
-   x1 <= y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2.
-intros x1 y1 x2 y2 a H H0 H1; try assumption.
-case H; intros.
-apply Rfourier_lt_le; auto with real.
-rewrite H2.
-apply Rplus_lt_compat_l.
-apply Rfourier_lt; auto with real.
-Qed.
-
-Lemma Rfourier_le_le :
- forall x1 y1 x2 y2 a:R,
-   x1 <= y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 <= y1 + a * y2.
-intros x1 y1 x2 y2 a H H0 H1; try assumption.
-case H0; intros.
-red.
-left; try assumption.
-apply Rfourier_le_lt; auto with real.
-rewrite H2.
-case H; intros.
-red.
-left; try assumption.
-rewrite (Rplus_comm x1 (a * y2)).
-rewrite (Rplus_comm y1 (a * y2)).
-apply Rplus_lt_compat_l.
-try exact H3.
-rewrite H3.
-red.
-right; try assumption.
-auto with real.
-Qed.
-
-Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x.
-intros x H; try assumption.
-rewrite Rplus_comm.
-apply Rle_lt_0_plus_1.
-red; auto with real.
-Qed.
-
-Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y.
-intros x y H H0; try assumption.
-replace 0 with (x * 0).
-apply Rmult_lt_compat_l; auto with real.
-ring.
-Qed.
-
-Lemma Rlt_zero_1 : 0 < 1.
-exact Rlt_0_1.
-Qed.
-
-Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x.
-intros x H; try assumption.
-case H; intros.
-red.
-left; try assumption.
-apply Rlt_zero_pos_plus1; auto with real.
-rewrite <- H0.
-replace (1 + 0) with 1.
-red; left.
-exact Rlt_zero_1.
-ring.
-Qed.
-
-Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y.
-intros x y H H0; try assumption.
-case H; intros.
-red; left.
-apply Rlt_mult_inv_pos; auto with real.
-rewrite <- H1.
-red; right; ring.
-Qed.
-
-Lemma Rle_zero_1 : 0 <= 1.
-red; left.
-exact Rlt_zero_1.
-Qed.
-
-Lemma Rle_not_lt : forall n d:R, 0 <= n * / d -> ~ 0 < - n * / d.
-intros n d H; red; intros H0; try exact H0.
-generalize (Rgt_not_le 0 (n * / d)).
-intros H1; elim H1; try assumption.
-replace (n * / d) with (- - (n * / d)).
-replace 0 with (- -0).
-replace (- (n * / d)) with (- n * / d).
-replace (-0) with 0.
-red.
-apply Ropp_gt_lt_contravar.
-red.
-exact H0.
-ring.
-ring.
-ring.
-ring.
-Qed.
-
-Lemma Rnot_lt0 : forall x:R, ~ 0 < 0 * x.
-intros x; try assumption.
-replace (0 * x) with 0.
-apply Rlt_irrefl.
-ring.
-Qed.
-
-Lemma Rlt_not_le_frac_opp : forall n d:R, 0 < n * / d -> ~ 0 <= - n * / d.
-intros n d H; try assumption.
-apply Rgt_not_le.
-replace 0 with (-0).
-replace (- n * / d) with (- (n * / d)).
-apply Ropp_lt_gt_contravar.
-try exact H.
-ring.
-ring.
-Qed.
-
-Lemma Rnot_lt_lt : forall x y:R, ~ 0 < y - x -> ~ x < y.
-unfold not; intros.
-apply H.
-apply Rplus_lt_reg_l with x.
-replace (x + 0) with x.
-replace (x + (y - x)) with y.
-try exact H0.
-ring.
-ring.
-Qed.
-
-Lemma Rnot_le_le : forall x y:R, ~ 0 <= y - x -> ~ x <= y.
-unfold not; intros.
-apply H.
-case H0; intros.
-left.
-apply Rplus_lt_reg_l with x.
-replace (x + 0) with x.
-replace (x + (y - x)) with y.
-try exact H1.
-ring.
-ring.
-right.
-rewrite H1; ring.
-Qed.
-
-Lemma Rfourier_gt_to_lt : forall x y:R, y > x -> x < y.
-unfold Rgt; intros; assumption.
-Qed.
-
-Lemma Rfourier_ge_to_le : forall x y:R, y >= x -> x <= y.
-intros x y; exact (Rge_le y x).
-Qed.
-
-Lemma Rfourier_eqLR_to_le : forall x y:R, x = y -> x <= y.
-exact Req_le.
-Qed.
-
-Lemma Rfourier_eqRL_to_le : forall x y:R, y = x -> x <= y.
-exact Req_le_sym.
-Qed.
-
-Lemma Rfourier_not_ge_lt : forall x y:R, (x >= y -> False) -> x < y.
-exact Rnot_ge_lt.
-Qed.
-
-Lemma Rfourier_not_gt_le : forall x y:R, (x > y -> False) -> x <= y.
-exact Rnot_gt_le.
-Qed.
-
-Lemma Rfourier_not_le_gt : forall x y:R, (x <= y -> False) -> x > y.
-exact Rnot_le_lt.
-Qed.
-
-Lemma Rfourier_not_lt_ge : forall x y:R, (x < y -> False) -> x >= y.
-exact Rnot_lt_ge.
-Qed.
diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml
deleted file mode 100644
index bee2b3b58..000000000
--- a/plugins/fourier/fourier.ml
+++ /dev/null
@@ -1,204 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* Méthode d'élimination de Fourier *)
-(* Référence:
-Auteur(s) : Fourier, Jean-Baptiste-Joseph
-
-Titre(s) : Oeuvres de Fourier [Document électronique]. Tome second. Mémoires publiés dans divers recueils / publ. par les soins de M. Gaston Darboux,...
-
-Publication : Numérisation BnF de l'édition de Paris : Gauthier-Villars, 1890
-
-Pages: 326-327
-
-http://gallica.bnf.fr/
-*)
-
-(* Un peu de calcul sur les rationnels...
-Les opérations rendent des rationnels normalisés,
-i.e. le numérateur et le dénominateur sont premiers entre eux.
-*)
-type rational = {num:int;
-                 den:int}
-;;
-let print_rational x =
-        print_int x.num;
-        print_string "/";
-        print_int x.den
-;;
-
-let rec pgcd x y = if y = 0 then x else pgcd y (x mod y);;
-
-
-let r0 = {num=0;den=1};;
-let r1 = {num=1;den=1};;
-
-let rnorm x = let x = (if x.den<0 then {num=(-x.num);den=(-x.den)} else x) in
-              if x.num=0 then r0
-              else (let d=pgcd x.num x.den in
-		    let d= (if d<0 then -d else d) in
-                    {num=(x.num)/d;den=(x.den)/d});;
-
-let rop x = rnorm {num=(-x.num);den=x.den};;
-
-let rplus x y = rnorm {num=x.num*y.den + y.num*x.den;den=x.den*y.den};;
-
-let rminus x y = rnorm {num=x.num*y.den - y.num*x.den;den=x.den*y.den};;
-
-let rmult x y = rnorm {num=x.num*y.num;den=x.den*y.den};;
-
-let rinv x = rnorm {num=x.den;den=x.num};;
-
-let rdiv x y = rnorm {num=x.num*y.den;den=x.den*y.num};;
-
-let rinf x y = x.num*y.den < y.num*x.den;;
-let rinfeq x y = x.num*y.den <= y.num*x.den;;
-
-(* {coef;hist;strict}, où coef=[c1; ...; cn; d], représente l'inéquation
-c1x1+...+cnxn < d si strict=true, <= sinon,
-hist donnant les coefficients (positifs) d'une combinaison linéaire qui permet d'obtenir l'inéquation à partir de celles du départ.
-*)
-
-type ineq = {coef:rational list;
-             hist:rational list;
-             strict:bool};;
-
-let pop x l = l:=x::(!l);;
-
-(* sépare la liste d'inéquations s selon que leur premier coefficient est
-négatif, nul ou positif. *)
-let partitionne s =
-   let lpos=ref [] in
-   let lneg=ref [] in
-   let lnul=ref [] in
-   List.iter (fun ie -> match ie.coef with
-                        [] ->  raise (Failure "empty ineq")
-                       |(c::r) -> if rinf c r0
-           	                  then pop ie lneg
-                                  else if rinf r0 c then pop ie lpos
-                                              else pop ie lnul)
-             s;
-   [!lneg;!lnul;!lpos]
-;;
-(* initialise les histoires d'une liste d'inéquations données par leurs listes de coefficients et leurs strictitudes (!):
-(add_hist [(equation 1, s1);...;(équation n, sn)])
-=
-[{équation 1, [1;0;...;0], s1};
- {équation 2, [0;1;...;0], s2};
- ...
- {équation n, [0;0;...;1], sn}]
-*)
-let add_hist le =
-   let n = List.length le in
-   let i = ref 0 in
-   List.map (fun (ie,s) ->
-              let h = ref [] in
-              for _k = 1 to (n - (!i) - 1) do pop r0 h; done;
-              pop r1 h;
-              for _k = 1 to !i do pop r0 h; done;
-              i:=!i+1;
-              {coef=ie;hist=(!h);strict=s})
-             le
-;;
-(* additionne deux inéquations *)
-let ie_add ie1 ie2 = {coef=List.map2 rplus ie1.coef ie2.coef;
-                      hist=List.map2 rplus ie1.hist ie2.hist;
-		      strict=ie1.strict || ie2.strict}
-;;
-(* multiplication d'une inéquation par un rationnel (positif) *)
-let ie_emult a ie = {coef=List.map (fun x -> rmult a x) ie.coef;
-                     hist=List.map (fun x -> rmult a x) ie.hist;
-		     strict= ie.strict}
-;;
-(* on enlève le premier coefficient *)
-let ie_tl ie = {coef=List.tl ie.coef;hist=ie.hist;strict=ie.strict}
-;;
-(* le premier coefficient: "tête" de l'inéquation *)
-let hd_coef ie = List.hd ie.coef
-;;
-
-(* calcule toutes les combinaisons entre inéquations de tête négative et inéquations de tête positive qui annulent le premier coefficient.
-*)
-let deduce_add lneg lpos =
-   let res=ref [] in
-   List.iter (fun i1 ->
-		 List.iter (fun i2 ->
-				let a = rop (hd_coef i1) in
-				let b = hd_coef i2 in
-				pop (ie_tl (ie_add (ie_emult b i1)
-						   (ie_emult a i2))) res)
-		           lpos)
-             lneg;
-   !res
-;;
-(* élimination de la première variable à partir d'une liste d'inéquations:
-opération qu'on itère dans l'algorithme de Fourier.
-*)
-let deduce1 s =
-    match (partitionne s) with
-      [lneg;lnul;lpos] ->
-    let lnew = deduce_add lneg lpos in
-    (List.map ie_tl lnul)@lnew
-     |_->assert false
-;;
-(* algorithme de Fourier: on élimine successivement toutes les variables.
-*)
-let deduce lie =
-   let n = List.length (fst (List.hd lie)) in
-   let lie=ref (add_hist lie) in
-   for _i = 1 to n - 1 do
-      lie:= deduce1 !lie;
-   done;
-   !lie
-;;
-
-(* donne [] si le système a des solutions,
-sinon donne [c,s,lc]
-où lc est la combinaison linéaire des inéquations de départ
-qui donne 0 < c si s=true
-       ou 0 <= c sinon
-cette inéquation étant absurde.
-*)
-
-exception Contradiction of (rational * bool * rational list) list
-
-let unsolvable lie =
-   let lr = deduce lie in
-   let check = function
-     | {coef=[c];hist=lc;strict=s} ->
-       if (rinf c r0 && (not s)) || (rinfeq c r0 && s)
-       then raise (Contradiction [c,s,lc])
-     |_->assert false
-   in
-   try List.iter check lr; []
-   with Contradiction l -> l
-
-(* Exemples:
-
-let test1=[[r1;r1;r0],true;[rop r1;r1;r1],false;[r0;rop r1;rop r1],false];;
-deduce test1;;
-unsolvable test1;;
-
-let test2=[
-[r1;r1;r0;r0;r0],false;
-[r0;r1;r1;r0;r0],false;
-[r0;r0;r1;r1;r0],false;
-[r0;r0;r0;r1;r1],false;
-[r1;r0;r0;r0;r1],false;
-[rop r1;rop r1;r0;r0;r0],false;
-[r0;rop r1;rop r1;r0;r0],false;
-[r0;r0;rop r1;rop r1;r0],false;
-[r0;r0;r0;rop r1;rop r1],false;
-[rop r1;r0;r0;r0;rop r1],false
-];;
-deduce test2;;
-unsolvable test2;;
-
-*)
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
deleted file mode 100644
index 96be1d893..000000000
--- a/plugins/fourier/fourierR.ml
+++ /dev/null
@@ -1,644 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-
-
-(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
-des inéquations et équations sont entiers. En attendant la tactique Field.
-*)
-
-open Constr
-open Tactics
-open Names
-open Globnames
-open Fourier
-open Contradiction
-open Proofview.Notations
-
-(******************************************************************************
-Opérations sur les combinaisons linéaires affines.
-La partie homogène d'une combinaison linéaire est en fait une table de hash
-qui donne le coefficient d'un terme du calcul des constructions,
-qui est zéro si le terme n'y est pas.
-*)
-
-module Constrhash = Hashtbl.Make(Constr)
-
-type flin = {fhom: rational Constrhash.t;
-             fcste:rational};;
-
-let flin_zero () = {fhom=Constrhash.create 50;fcste=r0};;
-
-let flin_coef f x = try Constrhash.find f.fhom x with Not_found -> r0;;
-
-let flin_add f x c =
-    let cx = flin_coef f x in
-    Constrhash.replace f.fhom x (rplus cx c);
-    f
-;;
-let flin_add_cste f c =
-    {fhom=f.fhom;
-     fcste=rplus f.fcste c}
-;;
-
-let flin_one () = flin_add_cste (flin_zero()) r1;;
-
-let flin_plus f1 f2 =
-    let f3 = flin_zero() in
-    Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
-    Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
-    flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
-;;
-
-let flin_minus f1 f2 =
-    let f3 = flin_zero() in
-    Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
-    Constrhash.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
-    flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
-;;
-let flin_emult a f =
-    let f2 = flin_zero() in
-    Constrhash.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
-    flin_add_cste f2 (rmult a f.fcste);
-;;
-
-(*****************************************************************************)
-
-type ineq = Rlt | Rle | Rgt | Rge
-
-let string_of_R_constant kn =
-  match Constant.repr3 kn with
-    | ModPath.MPfile dir, sec_dir, id when
-	sec_dir = DirPath.empty &&
-	DirPath.to_string dir = "Coq.Reals.Rdefinitions"
-	-> Label.to_string id
-    | _ -> "constant_not_of_R"
-
-let rec string_of_R_constr c =
- match Constr.kind c with
-   Cast (c,_,_) -> string_of_R_constr c
-  |Const (c,_) -> string_of_R_constant c
-  | _ -> "not_of_constant"
-
-exception NoRational
-
-let rec rational_of_constr c =
-  match Constr.kind c with
-  | Cast (c,_,_) -> (rational_of_constr c)
-  | App (c,args) ->
-      (match (string_of_R_constr c) with
-	 | "Ropp" ->
-	     rop (rational_of_constr args.(0))
-	 | "Rinv" ->
-	     rinv (rational_of_constr args.(0))
-	 | "Rmult" ->
-	     rmult (rational_of_constr args.(0))
-                   (rational_of_constr args.(1))
-	 | "Rdiv" ->
-	     rdiv (rational_of_constr args.(0))
-                  (rational_of_constr args.(1))
-	 | "Rplus" ->
-	     rplus (rational_of_constr args.(0))
-                   (rational_of_constr args.(1))
-	 | "Rminus" ->
-	     rminus (rational_of_constr args.(0))
-                    (rational_of_constr args.(1))
-	 | _ -> raise NoRational)
-  | Const (kn,_) ->
-      (match (string_of_R_constant kn) with
-	       "R1" -> r1
-              |"R0" -> r0
-              |  _ -> raise NoRational)
-  |  _ -> raise NoRational
-;;
-
-exception NoLinear
-
-let rec flin_of_constr c =
-  try(
-    match Constr.kind c with
-  | Cast (c,_,_) -> (flin_of_constr c)
-  | App (c,args) ->
-      (match (string_of_R_constr c) with
-	   "Ropp" ->
-             flin_emult (rop r1) (flin_of_constr args.(0))
-	 | "Rplus"->
-             flin_plus (flin_of_constr args.(0))
-	               (flin_of_constr args.(1))
-	 | "Rminus"->
-             flin_minus (flin_of_constr args.(0))
-	                (flin_of_constr args.(1))
-	 | "Rmult"->
-	     (try
-                let a = rational_of_constr args.(0) in
-                try
-                  let b = rational_of_constr args.(1) in
-		  flin_add_cste (flin_zero()) (rmult a b)
-		with NoRational ->
-                  flin_add (flin_zero()) args.(1) a
-	      with NoRational ->
-                flin_add (flin_zero()) args.(0)
-		  (rational_of_constr args.(1)))
-	 | "Rinv"->
-	     let a = rational_of_constr args.(0) in
-	     flin_add_cste (flin_zero()) (rinv a)
-	 | "Rdiv"->
-	     (let b = rational_of_constr args.(1) in
-	      try
-                let a = rational_of_constr args.(0) in
-	        flin_add_cste (flin_zero()) (rdiv a b)
-	      with NoRational ->
-                flin_add (flin_zero()) args.(0) (rinv b))
-         |_-> raise NoLinear)
-  | Const (c,_) ->
-        (match (string_of_R_constant c) with
-	       "R1" -> flin_one ()
-              |"R0" -> flin_zero ()
-              |_-> raise NoLinear)
-  |_-> raise NoLinear)
-  with NoRational | NoLinear -> flin_add (flin_zero()) c r1
-;;
-
-let flin_to_alist f =
-    let res=ref [] in
-    Constrhash.iter (fun x c -> res:=(c,x)::(!res)) f;
-    !res
-;;
-
-(* Représentation des hypothèses qui sont des inéquations ou des équations.
-*)
-type hineq={hname:constr; (* le nom de l'hypothèse *)
-            htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
-            hleft:constr;
-            hright:constr;
-            hflin:flin;
-            hstrict:bool}
-;;
-
-(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
-*)
-
-exception NoIneq
-
-let ineq1_of_constr (h,t) =
-  let h = EConstr.Unsafe.to_constr h in
-  let t = EConstr.Unsafe.to_constr t in
-    match (Constr.kind t) with
-      | App (f,args) ->
-        (match Constr.kind f with
-          | Const (c,_) when Array.length args = 2 ->
-            let t1= args.(0) in
-            let t2= args.(1) in
-            (match (string_of_R_constant c) with
-	      |"Rlt" -> [{hname=h;
-                           htype="Rlt";
-		           hleft=t1;
-			   hright=t2;
-			   hflin= flin_minus (flin_of_constr t1)
-                                             (flin_of_constr t2);
-			   hstrict=true}]
-	      |"Rgt" -> [{hname=h;
-                           htype="Rgt";
-		           hleft=t2;
-			   hright=t1;
-			   hflin= flin_minus (flin_of_constr t2)
-                                             (flin_of_constr t1);
-			   hstrict=true}]
-	      |"Rle" -> [{hname=h;
-                           htype="Rle";
-		           hleft=t1;
-			   hright=t2;
-			   hflin= flin_minus (flin_of_constr t1)
-                                             (flin_of_constr t2);
-			   hstrict=false}]
-	      |"Rge" -> [{hname=h;
-                           htype="Rge";
-		           hleft=t2;
-			   hright=t1;
-			   hflin= flin_minus (flin_of_constr t2)
-                                             (flin_of_constr t1);
-			   hstrict=false}]
-              |_-> raise NoIneq)
-          | Ind ((kn,i),_) ->
-            if not (GlobRef.equal (IndRef(kn,i)) Coqlib.glob_eq) then raise NoIneq;
-            let t0= args.(0) in
-            let t1= args.(1) in
-            let t2= args.(2) in
-	    (match (Constr.kind t0) with
-              | Const (c,_) ->
-		(match (string_of_R_constant c) with
-		  | "R"->
-                         [{hname=h;
-                           htype="eqTLR";
-		           hleft=t1;
-			   hright=t2;
-			   hflin= flin_minus (flin_of_constr t1)
-                                             (flin_of_constr t2);
-			   hstrict=false};
-                          {hname=h;
-                           htype="eqTRL";
-		           hleft=t2;
-			   hright=t1;
-			   hflin= flin_minus (flin_of_constr t2)
-                                             (flin_of_constr t1);
-			   hstrict=false}]
-                  |_-> raise NoIneq)
-              |_-> raise NoIneq)
-          |_-> raise NoIneq)
-      |_-> raise NoIneq
-;;
-
-(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
-*)
-
-let fourier_lineq lineq1 =
-   let nvar=ref (-1) in
-   let hvar=Constrhash.create 50 in (* la table des variables des inéquations *)
-   List.iter (fun f ->
-		Constrhash.iter (fun x _ -> if not (Constrhash.mem hvar x) then begin
-				nvar:=(!nvar)+1;
-				Constrhash.add hvar x (!nvar)
-			      end)
-                  f.hflin.fhom)
-             lineq1;
-   let sys= List.map (fun h->
-               let v=Array.make ((!nvar)+1) r0 in
-               Constrhash.iter (fun x c -> v.(Constrhash.find hvar x)<-c)
-                  h.hflin.fhom;
-               ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
-             lineq1 in
-   unsolvable sys
-;;
-
-(*********************************************************************)
-(* Defined constants *)
-
-let get = Lazy.force
-let cget = get
-let eget c = EConstr.of_constr (Lazy.force c)
-let constant path s = UnivGen.constr_of_global @@
-  Coqlib.coq_reference "Fourier" path s
-
-(* Standard library *)
-open Coqlib
-let coq_sym_eqT = lazy (build_coq_eq_sym ())
-let coq_False = lazy (UnivGen.constr_of_global @@ build_coq_False ())
-let coq_not = lazy (UnivGen.constr_of_global @@ build_coq_not ())
-let coq_eq = lazy (UnivGen.constr_of_global @@ build_coq_eq ())
-
-(* Rdefinitions *)
-let constant_real = constant ["Reals";"Rdefinitions"]
-
-let coq_Rlt = lazy (constant_real "Rlt")
-let coq_Rgt = lazy (constant_real "Rgt")
-let coq_Rle = lazy (constant_real "Rle")
-let coq_Rge = lazy (constant_real "Rge")
-let coq_R = lazy (constant_real "R")
-let coq_Rminus = lazy (constant_real "Rminus")
-let coq_Rmult = lazy (constant_real "Rmult")
-let coq_Rplus = lazy (constant_real "Rplus")
-let coq_Ropp = lazy (constant_real "Ropp")
-let coq_Rinv = lazy (constant_real "Rinv")
-let coq_R0 = lazy (constant_real "R0")
-let coq_R1 = lazy (constant_real "R1")
-
-(* RIneq *)
-let coq_Rinv_1 = lazy (constant ["Reals";"RIneq"] "Rinv_1")
-
-(* Fourier_util *)
-let constant_fourier = constant ["fourier";"Fourier_util"]
-
-let coq_Rlt_zero_1 = lazy (constant_fourier "Rlt_zero_1")
-let coq_Rlt_zero_pos_plus1 = lazy (constant_fourier "Rlt_zero_pos_plus1")
-let coq_Rle_zero_pos_plus1 = lazy (constant_fourier "Rle_zero_pos_plus1")
-let coq_Rlt_mult_inv_pos = lazy (constant_fourier "Rlt_mult_inv_pos")
-let coq_Rle_zero_zero = lazy (constant_fourier "Rle_zero_zero")
-let coq_Rle_zero_1 = lazy (constant_fourier "Rle_zero_1")
-let coq_Rle_mult_inv_pos = lazy (constant_fourier "Rle_mult_inv_pos")
-let coq_Rnot_lt0 = lazy (constant_fourier "Rnot_lt0")
-let coq_Rle_not_lt = lazy (constant_fourier "Rle_not_lt")
-let coq_Rfourier_gt_to_lt = lazy (constant_fourier "Rfourier_gt_to_lt")
-let coq_Rfourier_ge_to_le = lazy (constant_fourier "Rfourier_ge_to_le")
-let coq_Rfourier_eqLR_to_le = lazy (constant_fourier "Rfourier_eqLR_to_le")
-let coq_Rfourier_eqRL_to_le = lazy (constant_fourier "Rfourier_eqRL_to_le")
-
-let coq_Rfourier_not_ge_lt = lazy (constant_fourier "Rfourier_not_ge_lt")
-let coq_Rfourier_not_gt_le = lazy (constant_fourier "Rfourier_not_gt_le")
-let coq_Rfourier_not_le_gt = lazy (constant_fourier "Rfourier_not_le_gt")
-let coq_Rfourier_not_lt_ge = lazy (constant_fourier "Rfourier_not_lt_ge")
-let coq_Rfourier_lt = lazy (constant_fourier "Rfourier_lt")
-let coq_Rfourier_le = lazy (constant_fourier "Rfourier_le")
-let coq_Rfourier_lt_lt = lazy (constant_fourier "Rfourier_lt_lt")
-let coq_Rfourier_lt_le = lazy (constant_fourier "Rfourier_lt_le")
-let coq_Rfourier_le_lt = lazy (constant_fourier "Rfourier_le_lt")
-let coq_Rfourier_le_le = lazy (constant_fourier "Rfourier_le_le")
-let coq_Rnot_lt_lt = lazy (constant_fourier "Rnot_lt_lt")
-let coq_Rnot_le_le = lazy (constant_fourier "Rnot_le_le")
-let coq_Rlt_not_le_frac_opp = lazy (constant_fourier "Rlt_not_le_frac_opp")
-
-(******************************************************************************
-Construction de la preuve en cas de succès de la méthode de Fourier,
-i.e. on obtient une contradiction.
-*)
-let is_int x = (x.den)=1
-;;
-
-(* fraction = couple (num,den) *)
-let rational_to_fraction x= (x.num,x.den)
-;;
-
-(* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
-*)
-let int_to_real n =
-   let nn=abs n in
-   if nn=0
-   then get coq_R0
-   else
-     (let s=ref (get coq_R1) in
-      for _i = 1 to (nn-1) do s:=mkApp (get coq_Rplus,[|get coq_R1;!s|]) done;
-      if n<0 then mkApp (get coq_Ropp, [|!s|]) else !s)
-;;
-(* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
-*)
-let rational_to_real x =
-   let (n,d)=rational_to_fraction x in
-   mkApp (get coq_Rmult,
-     [|int_to_real n;mkApp(get coq_Rinv,[|int_to_real d|])|])
-;;
-
-(* preuve que 0<n*1/d
-*)
-let tac_zero_inf_pos gl (n,d) =
-  let get = eget in
-   let tacn=ref (apply (get coq_Rlt_zero_1)) in
-   let tacd=ref (apply (get coq_Rlt_zero_1)) in
-   for _i = 1 to n - 1 do
-       tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done;
-   for _i = 1 to d - 1 do
-       tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
-   (Tacticals.New.tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd])
-;;
-
-(* preuve que 0<=n*1/d
-*)
-let tac_zero_infeq_pos gl (n,d)=
-  let get = eget in
-   let tacn=ref (if n=0
-                 then (apply (get coq_Rle_zero_zero))
-                 else (apply (get coq_Rle_zero_1))) in
-   let tacd=ref (apply (get coq_Rlt_zero_1)) in
-   for  _i = 1 to n - 1 do
-       tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done;
-   for _i = 1 to d - 1 do
-       tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
-   (Tacticals.New.tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd])
-;;
-
-(* preuve que 0<(-n)*(1/d) => False
-*)
-let tac_zero_inf_false gl (n,d) =
-      let get = eget in
-if n=0 then (apply (get coq_Rnot_lt0))
-    else
-     (Tacticals.New.tclTHEN (apply (get coq_Rle_not_lt))
-	      (tac_zero_infeq_pos gl (-n,d)))
-;;
-
-(* preuve que 0<=(-n)*(1/d) => False
-*)
-let tac_zero_infeq_false gl (n,d) =
-  let get = eget in
-     (Tacticals.New.tclTHEN (apply (get coq_Rlt_not_le_frac_opp))
-	      (tac_zero_inf_pos gl (-n,d)))
-;;
-
-let exact = exact_check;;
-
-let tac_use h =
-  let get = eget in
-  let tac = exact (EConstr.of_constr h.hname) in
-  match h.htype with
-    "Rlt" -> tac
-  |"Rle" -> tac
-  |"Rgt" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac)
-  |"Rge" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac)
-  |"eqTLR" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac)
-  |"eqTRL" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac)
-  |_->assert false
-;;
-
-(*
-let is_ineq (h,t) =
-    match (Constr.kind t) with
-	App (f,args) ->
-	  (match (string_of_R_constr f) with
-	       "Rlt" -> true
-	     | "Rgt" -> true
-	     | "Rle" -> true
-	     | "Rge" -> true
-(* Wrong:not in Rdefinitions: *) | "eqT" ->
-                (match (string_of_R_constr args.(0)) with
-			     "R" -> true
-			   | _ -> false)
-             | _ ->false)
-      |_->false
-;;
-*)
-
-let list_of_sign s =
-  let open Context.Named.Declaration in
-  List.map (function LocalAssum (name, typ) -> name, typ
-                   | LocalDef (name, _, typ) -> name, typ)
-           s;;
-
-let mkAppL a =
-   let l = Array.to_list a in
-   mkApp(List.hd l, Array.of_list (List.tl l))
-;;
-
-exception GoalDone
-
-(* Résolution d'inéquations linéaires dans R *)
-let rec fourier () =
-  Proofview.Goal.nf_enter begin fun gl ->
-    let concl = Proofview.Goal.concl gl in
-    let sigma = Tacmach.New.project gl in
-    Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
-    let goal = Termops.strip_outer_cast sigma concl in
-    let goal = EConstr.Unsafe.to_constr goal in
-    let fhyp=Id.of_string "new_hyp_for_fourier" in
-    (* si le but est une inéquation, on introduit son contraire,
-       et le but à prouver devient False *)
-    try 
-      match (Constr.kind goal) with
-      App (f,args) ->
-      let get = eget in
-      (match (string_of_R_constr f) with
-	     "Rlt" ->
-	       (Tacticals.New.tclTHEN
-	         (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_ge_lt))
-			  (intro_using  fhyp))
-		 (fourier ()))
-	    |"Rle" ->
-	     (Tacticals.New.tclTHEN
-	      (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_gt_le))
-		       (intro_using  fhyp))
-			(fourier ()))
-	    |"Rgt" ->
-	     (Tacticals.New.tclTHEN
-	      (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_le_gt))
-		       (intro_using  fhyp))
-	      (fourier ()))
-	    |"Rge" ->
-	     (Tacticals.New.tclTHEN
-	      (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_lt_ge))
-		       (intro_using  fhyp))
-	      (fourier ()))
-	    |_-> raise GoalDone)
-        |_-> raise GoalDone
-     with GoalDone ->
-    (* les hypothèses *)
-    let hyps = List.map (fun (h,t)-> (EConstr.mkVar h,t))
-                        (list_of_sign (Proofview.Goal.hyps gl)) in
-    let lineq =ref [] in
-    List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
-		        with NoIneq -> ())
-              hyps;
-    (* lineq = les inéquations découlant des hypothèses *)
-    if !lineq=[] then CErrors.user_err Pp.(str "No inequalities");
-    let res=fourier_lineq (!lineq) in
-    let tac=ref (Proofview.tclUNIT ()) in
-    if res=[]
-    then CErrors.user_err Pp.(str "fourier failed")
-    (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
-    else (match res with
-        [(cres,sres,lc)]->
-    (* lc=coefficients multiplicateurs des inéquations
-       qui donnent 0<cres ou 0<=cres selon sres *)
-	(*print_string "Fourier's method can prove the goal...";flush stdout;*)
-          let lutil=ref [] in
-	  List.iter
-            (fun (h,c) ->
-			  if c<>r0
-        		  then (lutil:=(h,c)::(!lutil)(*;
-				print_rational(c);print_string " "*)))
-                    (List.combine (!lineq) lc);
-       (* on construit la combinaison linéaire des inéquation *)
-             (match (!lutil) with
-          (h1,c1)::lutil ->
-	  let s=ref (h1.hstrict) in
-	  let t1=ref (mkAppL [|get coq_Rmult;
-	                  rational_to_real c1;
-			  h1.hleft|]) in
-	  let t2=ref (mkAppL [|get coq_Rmult;
-	                  rational_to_real c1;
-			  h1.hright|]) in
-	  List.iter (fun (h,c) ->
-	       s:=(!s)||(h.hstrict);
-	       t1:=(mkAppL [|get coq_Rplus;
-	                     !t1;
-                             mkAppL [|get coq_Rmult;
-                                      rational_to_real c;
-			              h.hleft|] |]);
-	       t2:=(mkAppL [|get coq_Rplus;
-	                     !t2;
-                             mkAppL [|get coq_Rmult;
-                                      rational_to_real c;
-			              h.hright|] |]))
-               lutil;
-          let ineq=mkAppL [|if (!s) then get coq_Rlt else get coq_Rle;
-			      !t1;
-			      !t2 |] in
-	   let tc=rational_to_real cres in
-       (* puis sa preuve *)
-          let get = eget in
-           let tac1=ref (if h1.hstrict
-                         then (Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt))
-                                 [tac_use h1;
-                                  tac_zero_inf_pos  gl
-                                      (rational_to_fraction c1)])
-                         else (Tacticals.New.tclTHENS (apply (get coq_Rfourier_le))
-                                 [tac_use h1;
-				  tac_zero_inf_pos  gl
-                                      (rational_to_fraction c1)])) in
-           s:=h1.hstrict;
-           List.iter (fun (h,c)->
-             (if (!s)
-	      then (if h.hstrict
-	            then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_lt))
-			       [!tac1;tac_use h;
-			        tac_zero_inf_pos  gl
-                                      (rational_to_fraction c)])
-	            else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_le))
-			       [!tac1;tac_use h;
-			        tac_zero_inf_pos  gl
-                                      (rational_to_fraction c)]))
-	      else (if h.hstrict
-	            then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_lt))
-			       [!tac1;tac_use h;
-			        tac_zero_inf_pos  gl
-                                      (rational_to_fraction c)])
-	            else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_le))
-			       [!tac1;tac_use h;
-			        tac_zero_inf_pos  gl
-                                      (rational_to_fraction c)])));
-	     s:=(!s)||(h.hstrict))
-              lutil;
-           let tac2= if sres
-                      then tac_zero_inf_false gl (rational_to_fraction cres)
-                      else tac_zero_infeq_false gl (rational_to_fraction cres)
-           in
-           tac:=(Tacticals.New.tclTHENS (cut (EConstr.of_constr ineq))
-                     [Tacticals.New.tclTHEN (change_concl
-			       (EConstr.of_constr (mkAppL [| cget coq_not; ineq|]
-				       )))
-		      (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt
-					       else get coq_Rnot_le_le))
-			    (Tacticals.New.tclTHENS (Equality.replace
-				       (EConstr.of_constr (mkAppL [|cget coq_Rminus;!t2;!t1|]
-					       ))
-				       (EConstr.of_constr tc))
-		 	       [tac2;
-                                (Tacticals.New.tclTHENS
-				  (Equality.replace
-				    (EConstr.of_constr (mkApp (cget coq_Rinv,
-				      [|cget coq_R1|])))
-				    (get coq_R1))
-(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
-
-      			        [Tacticals.New.tclORELSE
-                                   (* TODO : Ring.polynom []*) (Proofview.tclUNIT ())
-                                   (Proofview.tclUNIT ());
-				 Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) >>= fun symeq ->
-					  (Tacticals.New.tclTHEN (apply symeq)
-						(apply (get coq_Rinv_1)))]
-
-					 )
-				]));
-                       !tac1]);
-	   tac:=(Tacticals.New.tclTHENS (cut (get coq_False))
-				  [Tacticals.New.tclTHEN intro (contradiction None);
-				   !tac])
-      |_-> assert false) |_-> assert false
-	  );
-(*    ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *)
-      !tac
-(*      ((tclABSTRACT None !tac) gl) *)
-  end
-;;
-
-(*
-let fourier_tac x gl =
-     fourier gl
-;;
-
-let v_fourier = add_tactic "Fourier" fourier_tac
-*)
-
diff --git a/plugins/fourier/fourier_plugin.mlpack b/plugins/fourier/fourier_plugin.mlpack
deleted file mode 100644
index b6262f8ae..000000000
--- a/plugins/fourier/fourier_plugin.mlpack
+++ /dev/null
@@ -1,3 +0,0 @@
-Fourier
-FourierR
-G_fourier
diff --git a/plugins/fourier/g_fourier.mlg b/plugins/fourier/g_fourier.mlg
deleted file mode 100644
index 703e29f96..000000000
--- a/plugins/fourier/g_fourier.mlg
+++ /dev/null
@@ -1,22 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-{
-
-open Ltac_plugin
-open FourierR
-
-}
-
-DECLARE PLUGIN "fourier_plugin"
-
-TACTIC EXTEND fourier
-| [ "fourierz" ] -> { fourier () }
-END
diff --git a/plugins/micromega/Fourier.v b/plugins/micromega/Fourier.v
new file mode 100644
index 000000000..0153de1da
--- /dev/null
+++ b/plugins/micromega/Fourier.v
@@ -0,0 +1,5 @@
+Require Import Lra.
+Require Export Fourier_util.
+
+#[deprecated(since = "8.9.0", note = "Use lra instead.")]
+Ltac fourier := lra.
diff --git a/plugins/micromega/Fourier_util.v b/plugins/micromega/Fourier_util.v
new file mode 100644
index 000000000..b62153dee
--- /dev/null
+++ b/plugins/micromega/Fourier_util.v
@@ -0,0 +1,31 @@
+Require Export Rbase.
+Require Import Lra.
+
+Open Scope R_scope.
+
+Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y.
+intros x y H H0; try assumption.
+replace 0 with (x * 0).
+apply Rmult_lt_compat_l; auto with real.
+ring.
+Qed.
+
+Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x.
+intros x H; try assumption.
+rewrite Rplus_comm.
+apply Rle_lt_0_plus_1.
+red; auto with real.
+Qed.
+
+Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x.
+  intros; lra.
+Qed.
+
+Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y.
+intros x y H H0; try assumption.
+case H; intros.
+red; left.
+apply Rlt_mult_inv_pos; auto with real.
+rewrite <- H1.
+red; right; ring.
+Qed.
diff --git a/test-suite/success/Fourier.v b/test-suite/success/LraTest.v
index b63bead47..bf3a87da2 100644
--- a/test-suite/success/Fourier.v
+++ b/test-suite/success/LraTest.v
@@ -1,12 +1,14 @@
-Require Import Rfunctions.
-Require Import Fourier.
+Require Import Reals.
+Require Import Lra.
+
+Open Scope R_scope.
 
 Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
-intros; split_Rabs; fourier.
+intros; split_Rabs; lra.
 Qed.
 
 Lemma l2 :
  forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1.
 intros.
-split_Rabs; fourier.
+split_Rabs; lra.
 Qed.
diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v
index cdf98cbde..8f7e07ac4 100644
--- a/theories/Reals/Machin.v
+++ b/theories/Reals/Machin.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Fourier.
+Require Import Lra.
 Require Import Rbase.
 Require Import Rtrigo1.
 Require Import Ranalysis_reg.
@@ -67,7 +67,7 @@ assert (atan x <= PI/4).
 assert (atan y < PI/4).
   rewrite <- atan_1; apply atan_increasing.
   assumption.
-rewrite Ropp_div; split; fourier.
+rewrite Ropp_div; split; lra.
 Qed.
 
 (* A simple formula, reasonably efficient. *)
@@ -77,8 +77,8 @@ assert (utility : 0 < PI/2) by (apply PI2_RGT_0).
 rewrite <- atan_1.
 rewrite (atan_sub_correct 1 (/2)).
    apply f_equal, f_equal; unfold atan_sub; field.
-  apply Rgt_not_eq; fourier.
- apply tech; try split; try fourier.
+  apply Rgt_not_eq; lra.
+ apply tech; try split; try lra.
 apply atan_bound.
 Qed.
 
@@ -86,7 +86,7 @@ Lemma Machin_4_5_239 : PI/4 = 4 * atan (/5) - atan(/239).
 Proof.
 rewrite <- atan_1.
 rewrite (atan_sub_correct 1 (/5));
- [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
+ [ | apply Rgt_not_eq; lra | apply tech; try split; lra |
      apply atan_bound ].
 replace (4 * atan (/5) - atan (/239)) with
   (atan (/5) + (atan (/5) + (atan (/5) + (atan (/5) + -
@@ -95,17 +95,17 @@ apply f_equal.
 replace (atan_sub 1 (/5)) with (2/3) by
   (unfold atan_sub; field).
 rewrite (atan_sub_correct (2/3) (/5));
- [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
+ [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra |
      apply atan_bound ].
 replace (atan_sub (2/3) (/5)) with (7/17)  by
   (unfold atan_sub; field).
 rewrite (atan_sub_correct (7/17) (/5));
- [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
+ [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra |
      apply atan_bound ].
 replace (atan_sub (7/17) (/5)) with (9/46) by
   (unfold atan_sub; field).
 rewrite (atan_sub_correct (9/46) (/5));
- [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
+ [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra |
      apply atan_bound ].
 rewrite <- atan_opp; apply f_equal.
 unfold atan_sub; field.
@@ -115,7 +115,7 @@ Lemma Machin_2_3_7 : PI/4 = 2 * atan(/3) + (atan (/7)).
 Proof.
 rewrite <- atan_1.
 rewrite (atan_sub_correct 1 (/3));
- [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
+ [ | apply Rgt_not_eq; lra | apply tech; try split; lra |
      apply atan_bound ].
 replace (2 * atan (/3) + atan (/7)) with
   (atan (/3) + (atan (/3) + atan (/7))) by ring.
@@ -123,7 +123,7 @@ apply f_equal.
 replace (atan_sub 1 (/3)) with (/2) by
   (unfold atan_sub; field).
 rewrite (atan_sub_correct (/2) (/3));
- [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
+ [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra |
      apply atan_bound ].
 apply f_equal; unfold atan_sub; field.
 Qed.
@@ -138,19 +138,19 @@ Lemma PI_2_3_7_ineq :
     sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <= PI / 4 <=
     sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N).
 Proof.
-assert (dec3 : 0 <= /3 <= 1) by (split; fourier).
-assert (dec7 : 0 <= /7 <= 1) by (split; fourier).
+assert (dec3 : 0 <= /3 <= 1) by (split; lra).
+assert (dec7 : 0 <= /7 <= 1) by (split; lra).
 assert (decr : Un_decreasing PI_2_3_7_tg).
  apply Ratan_seq_decreasing in dec3.
  apply Ratan_seq_decreasing in dec7.
  intros n; apply Rplus_le_compat.
-  apply Rmult_le_compat_l; [ fourier | exact (dec3 n)].
+  apply Rmult_le_compat_l; [ lra | exact (dec3 n)].
  exact (dec7 n).
 assert (cv : Un_cv PI_2_3_7_tg 0).
  apply Ratan_seq_converging in dec3.
  apply Ratan_seq_converging in dec7.
  intros eps ep.
- assert (ep' : 0 < eps /3) by fourier.
+ assert (ep' : 0 < eps /3) by lra.
  destruct (dec3 _ ep') as [N1 Pn1]; destruct (dec7 _ ep') as [N2 Pn2].
  exists (N1 + N2)%nat; intros n Nn.
  unfold PI_2_3_7_tg.
@@ -161,14 +161,14 @@ assert (cv : Un_cv PI_2_3_7_tg 0).
  apply Rplus_lt_compat.
   unfold R_dist, Rminus, Rdiv.
   rewrite <- (Rmult_0_r 2), <- Ropp_mult_distr_r_reverse.
-  rewrite <- Rmult_plus_distr_l, Rabs_mult, (Rabs_pos_eq 2);[|fourier].
-  rewrite Rmult_assoc; apply Rmult_lt_compat_l;[fourier | ].
+  rewrite <- Rmult_plus_distr_l, Rabs_mult, (Rabs_pos_eq 2);[|lra].
+  rewrite Rmult_assoc; apply Rmult_lt_compat_l;[lra | ].
    apply (Pn1 n); omega.
   apply (Pn2 n); omega.
 rewrite Machin_2_3_7.
-rewrite !atan_eq_ps_atan; try (split; fourier).
+rewrite !atan_eq_ps_atan; try (split; lra).
 unfold ps_atan; destruct (in_int (/3)); destruct (in_int (/7));
-  try match goal with id : ~ _ |- _ => case id; split; fourier end.
+  try match goal with id : ~ _ |- _ => case id; split; lra end.
 destruct (ps_atan_exists_1 (/3)) as [v3 Pv3].
 destruct (ps_atan_exists_1 (/7)) as [v7 Pv7].
 assert (main : Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg)) (2 * v3 + v7)).
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index 61d1b5afe..146d69101 100644
--- a/theories/Reals/PSeries_reg.v
+++ b/theories/Reals/PSeries_reg.v
@@ -15,7 +15,7 @@ Require Import Ranalysis1.
 Require Import MVT.
 Require Import Max.
 Require Import Even.
-Require Import Fourier.
+Require Import Lra.
 Local Open Scope R_scope.
 
 (* Boule is French for Ball *)
@@ -431,7 +431,7 @@ assert (ctrho : forall n z, Boule c d z -> continuity_pt (rho_ n) z).
   intros y dyz; unfold rho_; destruct (Req_EM_T y x) as [xy | xny].
    rewrite xy in dyz.
    destruct (Rle_dec  delta (Rabs (z - x))).
-    rewrite Rmin_left, R_dist_sym in dyz; unfold R_dist in dyz; fourier.
+    rewrite Rmin_left, R_dist_sym in dyz; unfold R_dist in dyz; lra.
    rewrite Rmin_right, R_dist_sym in dyz; unfold R_dist in dyz;
       [case (Rlt_irrefl _ dyz) |apply Rlt_le, Rnot_le_gt; assumption].
   reflexivity.
@@ -449,7 +449,7 @@ assert (ctrho : forall n z, Boule c d z -> continuity_pt (rho_ n) z).
 assert (CVU rho_ rho c d ).
  intros eps ep.
  assert (ep8 : 0 < eps/8).
-  fourier.
+  lra.
  destruct (cvu _ ep8) as [N Pn1].
  assert (cauchy1 : forall n p, (N <= n)%nat -> (N <= p)%nat ->
            forall z, Boule c d z -> Rabs (f' n z - f' p z) < eps/4).
@@ -537,7 +537,7 @@ assert (CVU rho_ rho c d ).
     simpl; unfold R_dist.
     unfold Rminus; rewrite (Rplus_comm y), Rplus_assoc, Rplus_opp_r, Rplus_0_r.
     rewrite Rabs_pos_eq;[ |apply Rlt_le; assumption ].
-    apply Rlt_le_trans with (Rmin (Rmin d' d2) delta);[fourier | ].
+    apply Rlt_le_trans with (Rmin (Rmin d' d2) delta);[lra | ].
     apply Rle_trans with (Rmin d' d2); apply Rmin_l.
    apply Rle_trans with (1 := R_dist_tri _ _ (rho_ p (y + Rmin (Rmin d' d2) delta/2))).
    apply Rplus_le_compat.
@@ -548,33 +548,32 @@ assert (CVU rho_ rho c d ).
      replace (rho_ p (y + Rmin (Rmin d' d2) delta / 2)) with
           ((f p (y + Rmin (Rmin d' d2) delta / 2) - f p x)/
              ((y + Rmin (Rmin d' d2) delta / 2) - x)).
-      apply step_2; auto; try fourier.
+      apply step_2; auto; try lra.
       assert (0 < pos delta) by (apply cond_pos).
       apply Boule_convex with y (y + delta/2).
         assumption.
        destruct (Pdelta (y + delta/2)); auto.
-       rewrite xy; unfold Boule; rewrite Rabs_pos_eq; try fourier; auto.
-      split; try fourier.
+       rewrite xy; unfold Boule; rewrite Rabs_pos_eq; try lra; auto.
+      split; try lra.
       apply Rplus_le_compat_l, Rmult_le_compat_r;[ | apply Rmin_r].
        now apply Rlt_le, Rinv_0_lt_compat, Rlt_0_2.
-      apply Rminus_not_eq_right; rewrite xy; apply Rgt_not_eq; fourier.
      unfold rho_.
      destruct (Req_EM_T (y + Rmin (Rmin d' d2) delta/2) x) as [ymx | ymnx].
-      case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); fourier.
+      case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); lra.
      reflexivity.
     unfold rho_.
     destruct (Req_EM_T (y + Rmin (Rmin d' d2) delta / 2) x) as [ymx | ymnx].
-     case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); fourier.
+     case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); lra.
     reflexivity.
-   apply Rlt_le, Pd2; split;[split;[exact I | apply Rlt_not_eq; fourier] | ].
+   apply Rlt_le, Pd2; split;[split;[exact I | apply Rlt_not_eq; lra] | ].
    simpl; unfold R_dist.
    unfold Rminus; rewrite (Rplus_comm y), Rplus_assoc, Rplus_opp_r, Rplus_0_r.
-   rewrite Rabs_pos_eq;[ | fourier].
-   apply Rlt_le_trans with (Rmin (Rmin d' d2) delta); [fourier |].
+   rewrite Rabs_pos_eq;[ | lra].
+   apply Rlt_le_trans with (Rmin (Rmin d' d2) delta); [lra |].
    apply Rle_trans with (Rmin d' d2).
     solve[apply Rmin_l].
    solve[apply Rmin_r].
-  apply Rlt_le, Rlt_le_trans with (eps/4);[ | fourier].
+  apply Rlt_le, Rlt_le_trans with (eps/4);[ | lra].
   unfold rho_; destruct (Req_EM_T y x); solve[auto].
  assert (unif_ac' : forall p, (N <= p)%nat ->
            forall y, Boule c d y -> Rabs (rho y - rho_ p y) < eps).
@@ -589,7 +588,7 @@ assert (CVU rho_ rho c d ).
    intros eps' ep'; simpl; exists 0%nat; intros; rewrite R_dist_eq; assumption.
   intros p pN y b_y.
   replace eps with (eps/2 + eps/2) by field.
-  assert (ep2 : 0 < eps/2) by fourier.
+  assert (ep2 : 0 < eps/2) by lra.
   destruct (cvrho y b_y _ ep2) as [N2 Pn2].
   apply Rle_lt_trans with (1 := R_dist_tri _ _ (rho_ (max N N2) y)).
   apply Rplus_lt_le_compat.
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index d4035fad6..6991923b1 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -155,6 +155,22 @@ Proof.
       | apply (sqrt_positivity x (Rlt_le 0 x H1)) ].
 Qed.
 
+Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y.
+intros x y H H0; try assumption.
+replace 0 with (x * 0).
+apply Rmult_lt_compat_l; auto with real.
+ring.
+Qed.
+
+Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y.
+intros x y H H0; try assumption.
+case H; intros.
+red; left.
+apply Rlt_mult_inv_pos; auto with real.
+rewrite <- H1.
+red; right; ring.
+Qed.
+
 Lemma sqrt_div_alt :
   forall x y : R, 0 < y -> sqrt (x / y) = sqrt x / sqrt y.
 Proof.
@@ -176,14 +192,14 @@ Proof.
   clearbody Hx'. clear Hx.
   apply Rsqr_inj.
   apply sqrt_pos.
-  apply Fourier_util.Rle_mult_inv_pos.
+  apply Rle_mult_inv_pos.
   apply Rsqrt_positivity.
   now apply sqrt_lt_R0.
   rewrite Rsqr_div, 2!Rsqr_sqrt.
   unfold Rsqr.
   now rewrite Rsqrt_Rsqrt.
   now apply Rlt_le.
-  now apply Fourier_util.Rle_mult_inv_pos.
+  now apply Rle_mult_inv_pos.
   apply Rgt_not_eq.
   now apply sqrt_lt_R0.
 Qed.
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index afb78e1c8..e66130b34 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -12,7 +12,7 @@ Require Import Rbase.
 Require Import Ranalysis_reg.
 Require Import Rfunctions.
 Require Import Rseries.
-Require Import Fourier.
+Require Import Lra.
 Require Import RiemannInt.
 Require Import SeqProp.
 Require Import Max.
@@ -56,7 +56,7 @@ Proof.
   }
   rewrite f_eq_g in Htemp by easy.
   unfold id in Htemp.
-  fourier.
+  lra.
 Qed.
 
 Lemma derivable_pt_id_interv : forall (lb ub x:R),
@@ -99,7 +99,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs
    apply Req_le ; apply Rabs_right ; apply Rgt_ge ; assumption.
  split.
  assert (Sublemma : forall x y z, -z < y - x -> x < y + z).
-  intros ; fourier.
+  intros ; lra.
  apply Sublemma.
  apply Sublemma2. rewrite Rabs_Ropp.
  apply Rlt_le_trans with (r2:=a-lb) ; [| apply RRle_abs] ;
@@ -108,7 +108,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs
  apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ;
  apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption.
  assert (Sublemma : forall x y z, y < z - x -> x + y < z).
-  intros ; fourier.
+  intros ; lra.
  apply Sublemma.
  apply Sublemma2.
  apply Rlt_le_trans with (r2:=ub-a) ; [| apply RRle_abs] ;
@@ -137,7 +137,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs
    apply Req_le ; apply Rabs_right ; apply Rgt_ge ; assumption.
  split.
  assert (Sublemma : forall x y z, -z < y - x -> x < y + z).
-  intros ; fourier.
+  intros ; lra.
  apply Sublemma.
  apply Sublemma2. rewrite Rabs_Ropp.
  apply Rlt_le_trans with (r2:=a-lb) ; [| apply RRle_abs] ;
@@ -146,7 +146,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs
  apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ;
  apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption.
  assert (Sublemma : forall x y z, y < z - x -> x + y < z).
-  intros ; fourier.
+  intros ; lra.
  apply Sublemma.
  apply Sublemma2.
  apply Rlt_le_trans with (r2:=ub-a) ; [| apply RRle_abs] ;
@@ -415,7 +415,7 @@ Ltac case_le H :=
    let h' := fresh in 
       match t with ?x <= ?y => case (total_order_T x y);
          [intros h'; case h'; clear h' | 
-          intros h'; clear -H h'; elimtype False; fourier ] end.
+          intros h'; clear -H h'; elimtype False; lra ] end.
 (* end hide *)
 
 
@@ -539,37 +539,37 @@ intros f g lb ub lb_lt_ub f_incr_interv f_eq_g f_cont_interv b b_encad.
  assert (x1_encad : lb <= x1 <= ub).
   split. apply RmaxLess2.
   apply Rlt_le. rewrite Hx1. rewrite Sublemma.
-  split. apply Rlt_trans with (r2:=x) ; fourier.
+  split. apply Rlt_trans with (r2:=x) ; lra.
   assumption.
  assert (x2_encad : lb <= x2 <= ub).
   split. apply Rlt_le ; rewrite Hx2 ; apply Rgt_lt ; rewrite Sublemma2.
-  split. apply Rgt_trans with (r2:=x) ; fourier.
+  split. apply Rgt_trans with (r2:=x) ; lra.
   assumption.
   apply Rmin_r.
  assert (x_lt_x2 : x < x2).
   rewrite Hx2.
   apply Rgt_lt. rewrite Sublemma2.
-  split ; fourier.
+  split ; lra.
  assert (x1_lt_x : x1 < x).
   rewrite Hx1.
   rewrite Sublemma.
-  split ; fourier.
+  split ; lra.
  exists (Rmin (f x - f x1) (f x2 - f x)).
- split. apply Rmin_pos ; apply Rgt_minus. apply f_incr_interv ; [apply RmaxLess2 | | ] ; fourier.
+ split. apply Rmin_pos ; apply Rgt_minus. apply f_incr_interv ; [apply RmaxLess2 | | ] ; lra.
  apply f_incr_interv ; intuition.
  intros y Temp.
  destruct Temp as (_,y_cond).
   rewrite <- f_x_b in y_cond.
   assert (Temp : forall x y d1 d2, d1 > 0 -> d2 > 0 -> Rabs (y - x) < Rmin d1 d2 -> x - d1 <= y <= x + d2).
    intros.
-    split. assert (H10 : forall x y z, x - y <= z -> x - z <= y). intuition. fourier.
+    split. assert (H10 : forall x y z, x - y <= z -> x - z <= y). intuition. lra.
     apply H10. apply Rle_trans with (r2:=Rabs (y0 - x0)).
     replace (Rabs (y0 - x0)) with (Rabs (x0 - y0)). apply RRle_abs.
     rewrite <- Rabs_Ropp. unfold Rminus ; rewrite Ropp_plus_distr. rewrite Ropp_involutive.
     intuition.
     apply Rle_trans with (r2:= Rmin d1 d2). apply Rlt_le ; assumption.
     apply Rmin_l.
-    assert (H10 : forall x y z, x - y <= z -> x <= y + z). intuition. fourier.
+    assert (H10 : forall x y z, x - y <= z -> x <= y + z). intuition. lra.
     apply H10. apply Rle_trans with (r2:=Rabs (y0 - x0)). apply RRle_abs.
     apply Rle_trans with (r2:= Rmin d1 d2). apply Rlt_le ; assumption.
     apply Rmin_r.
@@ -602,12 +602,12 @@ intros f g lb ub lb_lt_ub f_incr_interv f_eq_g f_cont_interv b b_encad.
      assert (x1_neq_x' : x1 <> x').
       intro Hfalse. rewrite Hfalse, f_x'_y in y_cond.
       assert (Hf : Rabs (y - f x) < f x - y).
-       apply Rlt_le_trans with (r2:=Rmin (f x - y) (f x2 - f x)). fourier.
+       apply Rlt_le_trans with (r2:=Rmin (f x - y) (f x2 - f x)). lra.
        apply Rmin_l.
       assert(Hfin : f x - y < f x - y).
        apply Rle_lt_trans with (r2:=Rabs (y - f x)).
        replace (Rabs (y - f x)) with (Rabs (f x - y)). apply RRle_abs.
-       rewrite <- Rabs_Ropp. replace (- (f x - y)) with (y - f x) by field ; reflexivity. fourier.
+       rewrite <- Rabs_Ropp. replace (- (f x - y)) with (y - f x) by field ; reflexivity. lra.
       apply (Rlt_irrefl (f x - y)) ; assumption.
       split ; intuition.
      assert (x'_lb : x - eps < x').
@@ -619,17 +619,17 @@ intros f g lb ub lb_lt_ub f_incr_interv f_eq_g f_cont_interv b b_encad.
      assert (x1_neq_x' : x' <> x2).
       intro Hfalse. rewrite <- Hfalse, f_x'_y in y_cond.
       assert (Hf : Rabs (y - f x) < y - f x).
-       apply Rlt_le_trans with (r2:=Rmin (f x - f x1) (y - f x)). fourier.
+       apply Rlt_le_trans with (r2:=Rmin (f x - f x1) (y - f x)). lra.
        apply Rmin_r.
       assert(Hfin : y - f x < y - f x).
-       apply Rle_lt_trans with (r2:=Rabs (y - f x)). apply RRle_abs. fourier.
+       apply Rle_lt_trans with (r2:=Rabs (y - f x)). apply RRle_abs. lra.
       apply (Rlt_irrefl (y - f x)) ; assumption.
       split ; intuition.
      assert (x'_ub : x' < x + eps).
       apply Sublemma3.
       split. intuition. apply Rlt_not_eq.
       apply Rlt_le_trans with (r2:=x2) ; [ |rewrite Hx2 ; apply Rmin_l] ; intuition.
-    apply Rabs_def1 ; fourier.
+    apply Rabs_def1 ; lra.
     assumption.
     split. apply Rle_trans with (r2:=x1) ; intuition.
     apply Rle_trans with (r2:=x2) ; intuition.
@@ -742,7 +742,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq.
  assert (lb <= x + h <= ub).
  split.
  assert (Sublemma : forall x y z, -z <= y - x -> x <= y + z).
-  intros ; fourier.
+  intros ; lra.
  apply Sublemma.
  apply Rlt_le ; apply Sublemma2. rewrite Rabs_Ropp.
  apply Rlt_le_trans with (r2:=x-lb) ; [| apply RRle_abs] ;
@@ -751,7 +751,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq.
  apply Rlt_le_trans with (r2:=delta''). assumption. intuition. apply Rmin_r.
  apply Rgt_minus. intuition.
  assert (Sublemma : forall x y z, y <= z - x -> x + y <= z).
-  intros ; fourier.
+  intros ; lra.
  apply Sublemma.
  apply Rlt_le ; apply Sublemma2.
  apply Rlt_le_trans with (r2:=ub-x) ; [| apply RRle_abs] ;
@@ -767,7 +767,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq.
  assumption.
          split ; [|intuition].
          assert (Sublemma : forall x y z, - z <= y - x -> x <= y + z).
-          intros ; fourier.
+          intros ; lra.
          apply Sublemma ; apply Rlt_le ; apply Sublemma2. rewrite Rabs_Ropp.
  apply Rlt_le_trans with (r2:=x-lb) ; [| apply RRle_abs] ;
  apply Rlt_le_trans with (r2:=Rmin (x - lb) (ub - x)) ; [| apply Rmin_l] ;
@@ -1031,7 +1031,7 @@ Lemma derivable_pt_lim_CVU : forall (fn fn':nat -> R -> R) (f g:R->R)
       derivable_pt_lim f x (g x).
 Proof.
 intros fn fn' f g x c' r xinb Dfn_eq_fn' fn_CV_f fn'_CVU_g g_cont eps eps_pos.
-assert (eps_8_pos : 0 < eps / 8) by fourier.
+assert (eps_8_pos : 0 < eps / 8) by lra.
 elim (g_cont x xinb _ eps_8_pos) ; clear g_cont ;
 intros delta1 (delta1_pos, g_cont).
 destruct (Ball_in_inter _ _ _ _ _ xinb
@@ -1041,11 +1041,11 @@ exists delta; intros h hpos hinbdelta.
 assert (eps'_pos : 0 < (Rabs h) * eps / 4).
  unfold Rdiv ; rewrite Rmult_assoc ; apply Rmult_lt_0_compat.
  apply Rabs_pos_lt ; assumption.
-fourier.
+lra.
 destruct (fn_CV_f x xinb ((Rabs h) * eps / 4) eps'_pos) as [N2 fnx_CV_fx].
 assert (xhinbxdelta : Boule x delta (x + h)).
  clear -hinbdelta; apply Rabs_def2 in hinbdelta; unfold Boule; simpl.
- destruct hinbdelta; apply Rabs_def1; fourier.
+ destruct hinbdelta; apply Rabs_def1; lra.
 assert (t : Boule c' r (x + h)).
  apply Pdelta in xhinbxdelta; tauto.
 destruct (fn_CV_f (x+h) t ((Rabs h) * eps / 4) eps'_pos) as [N1 fnxh_CV_fxh].
@@ -1064,17 +1064,17 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn
    exists (fn' N c) ; apply Dfn_eq_fn'.
    assert (t : Boule x delta c).
     apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta; destruct c_encad.
-    apply Rabs_def2 in xinb; apply Rabs_def1; fourier.
+    apply Rabs_def2 in xinb; apply Rabs_def1; lra.
    apply Pdelta in t; tauto.
   assert (pr2 : forall c : R, x + h < c < x -> derivable_pt id c).
    solve[intros; apply derivable_id].
-  assert (xh_x : x+h < x) by fourier.
+  assert (xh_x : x+h < x) by lra.
   assert (pr3 : forall c : R, x + h <= c <= x -> continuity_pt (fn N) c).
    intros c c_encad ; apply derivable_continuous_pt.
    exists (fn' N c) ; apply Dfn_eq_fn' ; intuition.
    assert (t : Boule x delta c).
     apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta.
-    apply Rabs_def2 in xinb; apply Rabs_def1; fourier.
+    apply Rabs_def2 in xinb; apply Rabs_def1; lra.
    apply Pdelta in t; tauto.
   assert (pr4 : forall c : R, x + h <= c <= x -> continuity_pt id c).
    solve[intros; apply derivable_continuous ; apply derivable_id].
@@ -1117,7 +1117,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn
     assert (t : Boule x delta c).
      destruct P.
      apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta.
-     apply Rabs_def2 in xinb; apply Rabs_def1; fourier.
+     apply Rabs_def2 in xinb; apply Rabs_def1; lra.
     apply Pdelta in t; tauto.
    apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * (eps / 8) +
          Rabs h * (eps / 8)).
@@ -1131,27 +1131,27 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn
     apply Rlt_trans with (Rabs h).
      apply Rabs_def1. 
       apply Rlt_trans with 0.
-       destruct P; fourier.
+       destruct P; lra.
       apply Rabs_pos_lt ; assumption.
-     rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_involutive;[ | fourier]. 
-     destruct P; fourier.
+     rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_involutive;[ | lra].
+     destruct P; lra.
     clear -Pdelta xhinbxdelta.
     apply Pdelta in xhinbxdelta; destruct xhinbxdelta as [_ P'].
     apply Rabs_def2 in P'; simpl in P'; destruct P';
-    apply Rabs_def1; fourier.
+    apply Rabs_def1; lra.
    rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite <- Rmult_plus_distr_l.
    replace (Rabs h * eps / 4 + (Rabs h * eps / 4 + Rabs h * (eps / 8 + eps / 8))) with
       (Rabs h * (eps / 4 + eps / 4 + eps / 8 + eps / 8)) by field.
    apply Rmult_lt_compat_l. 
     apply Rabs_pos_lt ; assumption.
-   fourier.
+   lra.
   assert (H := pr1 c P) ; elim H ; clear H ; intros l Hl.
   assert (Temp : l = fn' N c).
    assert (bc'rc : Boule c' r c).
     assert (t : Boule x delta c).
      clear - xhinbxdelta P.
      destruct P; apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta.
-     apply Rabs_def1; fourier.
+     apply Rabs_def1; lra.
     apply Pdelta in t; tauto.
    assert (Hl' := Dfn_eq_fn' c N bc'rc).
    unfold derivable_pt_abs in Hl; clear -Hl Hl'.
@@ -1175,17 +1175,17 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn
   exists (fn' N c) ; apply Dfn_eq_fn'.
   assert (t : Boule x delta c).
    apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta; destruct c_encad.
-   apply Rabs_def2 in xinb; apply Rabs_def1; fourier.
+   apply Rabs_def2 in xinb; apply Rabs_def1; lra.
   apply Pdelta in t; tauto.
   assert (pr2 : forall c : R, x < c < x + h -> derivable_pt id c).
    solve[intros; apply derivable_id].
-  assert (xh_x : x < x + h) by fourier.
+  assert (xh_x : x < x + h) by lra.
   assert (pr3 : forall c : R, x <= c <= x + h -> continuity_pt (fn N) c).
    intros c c_encad ; apply derivable_continuous_pt.
    exists (fn' N c) ; apply Dfn_eq_fn' ; intuition.
    assert (t : Boule x delta c).
     apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta.
-    apply Rabs_def2 in xinb; apply Rabs_def1; fourier.
+    apply Rabs_def2 in xinb; apply Rabs_def1; lra.
    apply Pdelta in t; tauto.
   assert (pr4 : forall c : R, x <= c <= x + h -> continuity_pt id c).
    solve[intros; apply derivable_continuous ; apply derivable_id].
@@ -1223,7 +1223,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn
     assert (t : Boule x delta c).
      destruct P.
     apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta.
-    apply Rabs_def2 in xinb; apply Rabs_def1; fourier.
+    apply Rabs_def2 in xinb; apply Rabs_def1; lra.
    apply Pdelta in t; tauto.
   apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * (eps / 8) +
          Rabs h * (eps / 8)).
@@ -1236,27 +1236,27 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn
     apply Rlt_not_eq ; exact (proj1 P).
    apply Rlt_trans with (Rabs h).
     apply Rabs_def1.
-     destruct P; rewrite Rabs_pos_eq;fourier.
+     destruct P; rewrite Rabs_pos_eq;lra.
     apply Rle_lt_trans with 0.
-     assert (t := Rabs_pos h); clear -t; fourier.
-    clear -P; destruct P; fourier.
+     assert (t := Rabs_pos h); clear -t; lra.
+    clear -P; destruct P; lra.
    clear -Pdelta xhinbxdelta.
    apply Pdelta in xhinbxdelta; destruct xhinbxdelta as [_ P'].
    apply Rabs_def2 in P'; simpl in P'; destruct P';
-    apply Rabs_def1; fourier.
+    apply Rabs_def1; lra.
   rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite <- Rmult_plus_distr_l.
   replace (Rabs h * eps / 4 + (Rabs h * eps / 4 + Rabs h * (eps / 8 + eps / 8))) with
       (Rabs h * (eps / 4 + eps / 4 + eps / 8 + eps / 8)) by field.
   apply Rmult_lt_compat_l. 
    apply Rabs_pos_lt ; assumption.
-  fourier.
+  lra.
  assert (H := pr1 c P) ; elim H ; clear H ; intros l Hl.
  assert (Temp : l = fn' N c).
   assert (bc'rc : Boule c' r c).
    assert (t : Boule x delta c).
     clear - xhinbxdelta P.
     destruct P; apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta.
-    apply Rabs_def1; fourier.
+    apply Rabs_def1; lra.
    apply Pdelta in t; tauto.
   assert (Hl' := Dfn_eq_fn' c N bc'rc).
   unfold derivable_pt_abs in Hl; clear -Hl Hl'.
diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v
index ce39d5ffe..03e6ff61a 100644
--- a/theories/Reals/Ratan.v
+++ b/theories/Reals/Ratan.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Fourier.
+Require Import Lra.
 Require Import Rbase.
 Require Import PSeries_reg.
 Require Import Rtrigo1.
@@ -32,7 +32,7 @@ intros x y; unfold Rdiv; rewrite <-Ropp_mult_distr_l_reverse; reflexivity.
 Qed.
 
 Definition pos_half_prf : 0 < /2.
-Proof. fourier. Qed.
+Proof. lra. Qed.
 
 Definition pos_half := mkposreal (/2) pos_half_prf.
 
@@ -40,15 +40,15 @@ Lemma Boule_half_to_interval :
   forall x , Boule (/2) pos_half x -> 0 <= x <= 1.
 Proof.
 unfold Boule, pos_half; simpl.
-intros x b; apply Rabs_def2 in b; destruct b; split; fourier.
+intros x b; apply Rabs_def2 in b; destruct b; split; lra.
 Qed.
 
 Lemma Boule_lt : forall c r x, Boule c r x -> Rabs x < Rabs c + r.
 Proof.
 unfold Boule; intros c r x h.
 apply Rabs_def2 in h; destruct h; apply Rabs_def1;
- (destruct (Rle_lt_dec 0 c);[rewrite Rabs_pos_eq; fourier | 
-    rewrite <- Rabs_Ropp, Rabs_pos_eq; fourier]).
+ (destruct (Rle_lt_dec 0 c);[rewrite Rabs_pos_eq; lra |
+    rewrite <- Rabs_Ropp, Rabs_pos_eq; lra]).
 Qed.
 
 (* The following lemma does not belong here. *)
@@ -117,53 +117,53 @@ intros [ | N] Npos n decr to0 cv nN.
   case (even_odd_cor n) as [p' [neven | nodd]].
    rewrite neven.
    destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E].
-   unfold R_dist; rewrite Rabs_pos_eq;[ | fourier].
+   unfold R_dist; rewrite Rabs_pos_eq;[ | lra].
    assert (dist : (p <= p')%nat) by omega.
    assert (t := decreasing_prop _ _ _ (CV_ALT_step1 f decr) dist).
    apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * p) - l).
     unfold Rminus; apply Rplus_le_compat_r; exact t.
    match goal with _ : ?a <= l, _ : l <= ?b |- _ => 
     replace (f (S (2 * p))) with (b - a) by
-     (rewrite tech5; unfold tg_alt; rewrite pow_1_odd; ring); fourier
+     (rewrite tech5; unfold tg_alt; rewrite pow_1_odd; ring); lra
    end.
   rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E].
    unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_minus_distr;
-     [ | fourier].
+     [ | lra].
    assert (dist : (p <= p')%nat) by omega.
    apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))).
     unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar.
     solve[apply Rge_le, (growing_prop _ _ _ (CV_ALT_step0 f decr) dist)].
    unfold Rminus; rewrite tech5, Ropp_plus_distr, <- Rplus_assoc.
-   unfold tg_alt at 2; rewrite pow_1_odd; fourier.
+   unfold tg_alt at 2; rewrite pow_1_odd; lra.
  rewrite Nodd; destruct (alternated_series_ineq _ _ p decr to0 cv) as [B _].
  destruct (alternated_series_ineq _ _ (S p) decr to0 cv) as [_ C].
  assert (keep : (2 * S p = S (S ( 2 * p)))%nat) by ring.
  case (even_odd_cor n) as [p' [neven | nodd]].
    rewrite neven;
    destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E].
-   unfold R_dist; rewrite Rabs_pos_eq;[ | fourier].
+   unfold R_dist; rewrite Rabs_pos_eq;[ | lra].
    assert (dist : (S p < S p')%nat) by omega.
    apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * S p) - l).
    unfold Rminus; apply Rplus_le_compat_r,
      (decreasing_prop _ _ _ (CV_ALT_step1 f decr)).
    omega.
   rewrite keep, tech5; unfold tg_alt at 2; rewrite <- keep, pow_1_even.
-  fourier.
+  lra.
  rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E].
- unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq;[ | fourier].
+ unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq;[ | lra].
  rewrite Ropp_minus_distr.
  apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))).
   unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar, Rge_le,
    (growing_prop _ _ _ (CV_ALT_step0 f decr)); omega.
  generalize C; rewrite keep, tech5; unfold tg_alt.
  rewrite <- keep, pow_1_even.
- assert (t : forall a b c, a <= b + 1 * c -> a - b <= c) by (intros; fourier).
+ assert (t : forall a b c, a <= b + 1 * c -> a - b <= c) by (intros; lra).
  solve[apply t].
 clear WLOG; intros Hyp [ | n] decr to0 cv _.
  generalize (alternated_series_ineq f l 0 decr to0 cv).
  unfold R_dist, tg_alt; simpl; rewrite !Rmult_1_l, !Rmult_1_r.
  assert (f 1%nat <= f 0%nat) by apply decr.
- intros [A B]; rewrite Rabs_pos_eq; fourier.
+ intros [A B]; rewrite Rabs_pos_eq; lra.
 apply Rle_trans with (f 1%nat).
  apply (Hyp 1%nat (le_n 1) (S n) decr to0 cv).
  omega.
@@ -180,7 +180,7 @@ Lemma Alt_CVU : forall (f : nat -> R -> R) g h c r,
    CVU (fun N x => sum_f_R0 (tg_alt (fun i => f i x)) N) g c r.
 Proof.
 intros f g h c r decr to0 to_g bound bound0 eps ep.  
-assert (ep' : 0 <eps/2) by fourier.
+assert (ep' : 0 <eps/2) by lra.
 destruct (bound0 _ ep) as [N Pn]; exists N.
 intros n y nN dy.
 rewrite <- Rabs_Ropp, Ropp_minus_distr; apply Rle_lt_trans with (f n y).
@@ -201,14 +201,14 @@ intros x; destruct (Rle_lt_dec 0 x).
  replace (x ^ 2) with (x * x) by field.
  apply Rmult_le_pos; assumption.
  replace (x ^ 2) with ((-x) * (-x)) by field.
-apply Rmult_le_pos; fourier.
+apply Rmult_le_pos; lra.
 Qed.
 
 Lemma pow2_abs : forall x,  Rabs x ^ 2 = x ^ 2.
 Proof.
 intros x; destruct (Rle_lt_dec 0 x).
  rewrite Rabs_pos_eq;[field | assumption].
-rewrite <- Rabs_Ropp, Rabs_pos_eq;[field | fourier].
+rewrite <- Rabs_Ropp, Rabs_pos_eq;[field | lra].
 Qed.
 
 (** * Properties of tangent *)
@@ -307,18 +307,18 @@ destruct (MVT_cor1 cos (PI/2) x derivable_cos xgtpi2) as
    [c [Pc [cint1 cint2]]].
 revert Pc; rewrite cos_PI2, Rminus_0_r. 
 rewrite <- (pr_nu cos c (derivable_pt_cos c)), derive_pt_cos.
-assert (0 < c < 2) by (split; assert (t := PI2_RGT_0); fourier).
+assert (0 < c < 2) by (split; assert (t := PI2_RGT_0); lra).
 assert (0 < sin c) by now apply sin_pos_tech.
 intros Pc.
 case (Rlt_not_le _ _ cx).
 rewrite <- (Rplus_0_l (cos x)), Pc, Ropp_mult_distr_l_reverse.
-apply Rle_minus, Rmult_le_pos;[apply Rlt_le; assumption | fourier ].
+apply Rle_minus, Rmult_le_pos;[apply Rlt_le; assumption | lra ].
 Qed.
 
 Lemma PI2_3_2 : 3/2 < PI/2.
 Proof.
-apply PI2_lower_bound;[split; fourier | ].
-destruct (pre_cos_bound (3/2) 1) as [t _]; [fourier | fourier | ].
+apply PI2_lower_bound;[split; lra | ].
+destruct (pre_cos_bound (3/2) 1) as [t _]; [lra | lra | ].
 apply Rlt_le_trans with (2 := t); clear t.
 unfold cos_approx; simpl; unfold cos_term.
 rewrite !INR_IZR_INZ.
@@ -330,7 +330,7 @@ apply Rdiv_lt_0_compat ; now apply IZR_lt.
 Qed.
 
 Lemma PI2_1 : 1 < PI/2.
-Proof. assert (t := PI2_3_2); fourier. Qed.
+Proof. assert (t := PI2_3_2); lra. Qed.
 
 Lemma tan_increasing :
   forall x y:R,
@@ -347,7 +347,7 @@ intros x y Z_le_x x_lt_y y_le_1.
           derivable_pt tan x).
   intros ; apply derivable_pt_tan ; intuition.
  apply derive_increasing_interv with (a:=-PI/2) (b:=PI/2) (pr:=local_derivable_pt_tan) ; intuition.
- fourier.
+ lra.
  assert (Temp := pr_nu tan t (derivable_pt_tan t t_encad) (local_derivable_pt_tan t t_encad)) ;
  rewrite <- Temp ; clear Temp.
  assert (Temp := derive_pt_tan t t_encad) ; rewrite Temp ; clear Temp.
@@ -414,49 +414,49 @@ Qed.
 (** * Definition of arctangent as the reciprocal function of tangent and proof of this status *)
 Lemma tan_1_gt_1 : tan 1 > 1.
 Proof.
-assert (0 < cos 1) by (apply cos_gt_0; assert (t:=PI2_1); fourier).
+assert (0 < cos 1) by (apply cos_gt_0; assert (t:=PI2_1); lra).
 assert (t1 : cos 1 <= 1 - 1/2 + 1/24).
- destruct (pre_cos_bound 1 0) as [_ t]; try fourier; revert t.
+ destruct (pre_cos_bound 1 0) as [_ t]; try lra; revert t.
  unfold cos_approx, cos_term; simpl; intros t; apply Rle_trans with (1:=t).
  clear t; apply Req_le; field.
 assert (t2 : 1 - 1/6 <= sin 1).
- destruct (pre_sin_bound 1 0) as [t _]; try fourier; revert t.
+ destruct (pre_sin_bound 1 0) as [t _]; try lra; revert t.
  unfold sin_approx, sin_term; simpl; intros t; apply Rle_trans with (2:=t).
  clear t; apply Req_le; field.
 pattern 1 at 2; replace 1 with
-  (cos 1 / cos 1) by (field; apply Rgt_not_eq; fourier).
+  (cos 1 / cos 1) by (field; apply Rgt_not_eq; lra).
 apply Rlt_gt; apply (Rmult_lt_compat_r (/ cos 1) (cos 1) (sin 1)).
  apply Rinv_0_lt_compat; assumption.
 apply Rle_lt_trans with (1 := t1); apply Rlt_le_trans with (2 := t2).
-fourier.
+lra.
 Qed.
 
 Definition frame_tan y : {x | 0 < x < PI/2 /\ Rabs y < tan x}.
 Proof.
 destruct (total_order_T (Rabs y) 1) as [Hs|Hgt].
- assert (yle1 : Rabs y <= 1) by (destruct Hs; fourier).
+ assert (yle1 : Rabs y <= 1) by (destruct Hs; lra).
  clear Hs; exists 1; split;[split; [exact Rlt_0_1 | exact PI2_1] | ].
  apply Rle_lt_trans with (1 := yle1); exact tan_1_gt_1.
 assert (0 < / (Rabs y + 1)).
- apply Rinv_0_lt_compat; fourier.
+ apply Rinv_0_lt_compat; lra.
 set (u := /2 * / (Rabs y + 1)).
 assert (0 < u).
- apply Rmult_lt_0_compat; [fourier | assumption].
+ apply Rmult_lt_0_compat; [lra | assumption].
 assert (vlt1 : / (Rabs y + 1) < 1).
  apply Rmult_lt_reg_r with (Rabs y + 1).
-  assert (t := Rabs_pos y); fourier.
- rewrite Rinv_l; [rewrite Rmult_1_l | apply Rgt_not_eq]; fourier.
+  assert (t := Rabs_pos y); lra.
+ rewrite Rinv_l; [rewrite Rmult_1_l | apply Rgt_not_eq]; lra.
 assert (vlt2 : u < 1).
  apply Rlt_trans with (/ (Rabs y + 1)).
   rewrite double_var.
-  assert (t : forall x, 0 < x -> x < x + x) by (clear; intros; fourier).
+  assert (t : forall x, 0 < x -> x < x + x) by (clear; intros; lra).
   unfold u; rewrite Rmult_comm; apply t.
   unfold Rdiv; rewrite Rmult_comm; assumption.
  assumption.
 assert(int : 0 < PI / 2 - u < PI / 2).
  split.
   assert (t := PI2_1); apply Rlt_Rminus, Rlt_trans with (2 := t); assumption.
- assert (dumb : forall x y, 0 < y -> x - y < x) by (clear; intros; fourier).
+ assert (dumb : forall x y, 0 < y -> x - y < x) by (clear; intros; lra).
  apply dumb; clear dumb; assumption.
 exists (PI/2 - u).
 assert (tmp : forall x y, 0 < x -> y < 1 -> x * y < x).
@@ -473,7 +473,7 @@ split.
  assert (sin u < u).
   assert (t1 : 0 <= u) by (apply Rlt_le; assumption).
   assert (t2 : u <= 4) by
-   (apply Rle_trans with 1;[apply Rlt_le | fourier]; assumption).
+   (apply Rle_trans with 1;[apply Rlt_le | lra]; assumption).
   destruct (pre_sin_bound u 0 t1 t2) as [_ t].
   apply Rle_lt_trans with (1 := t); clear t1 t2 t.
   unfold sin_approx; simpl; unfold sin_term; simpl ((-1) ^ 0);
@@ -503,17 +503,17 @@ split.
    solve[apply Rinv_0_lt_compat, INR_fact_lt_0].
   apply Rlt_trans with (2 := vlt2).
   simpl; unfold u; apply tmp; auto; rewrite Rmult_1_r; assumption.
- apply Rlt_trans with (Rabs y + 1);[fourier | ]. 
+ apply Rlt_trans with (Rabs y + 1);[lra | ].
  pattern (Rabs y + 1) at 1; rewrite <- (Rinv_involutive (Rabs y + 1));
-  [ | apply Rgt_not_eq; fourier].
+  [ | apply Rgt_not_eq; lra].
  rewrite <- Rinv_mult_distr.
    apply Rinv_lt_contravar.
     apply Rmult_lt_0_compat.
-     apply Rmult_lt_0_compat;[fourier | assumption].
+     apply Rmult_lt_0_compat;[lra | assumption].
     assumption.
    replace (/(Rabs y + 1)) with (2 * u).
-    fourier.
-   unfold u; field; apply Rgt_not_eq; clear -Hgt; fourier.
+    lra.
+   unfold u; field; apply Rgt_not_eq; clear -Hgt; lra.
   solve[discrR].
  apply Rgt_not_eq; assumption.
 unfold tan.
@@ -522,22 +522,22 @@ set (u' := PI / 2); unfold Rdiv; apply Rmult_lt_compat_r; unfold u'.
  rewrite cos_shift; assumption.
 assert (vlt3 : u < /4).
  replace (/4) with (/2 * /2) by field.
- unfold u; apply Rmult_lt_compat_l;[fourier | ].
+ unfold u; apply Rmult_lt_compat_l;[lra | ].
  apply Rinv_lt_contravar.
-  apply Rmult_lt_0_compat; fourier.
- fourier.
-assert (1 < PI / 2 - u) by (assert (t := PI2_3_2); fourier).
+  apply Rmult_lt_0_compat; lra.
+ lra.
+assert (1 < PI / 2 - u) by (assert (t := PI2_3_2); lra).
 apply Rlt_trans with (sin 1).
- assert (t' : 1 <= 4) by fourier.
+ assert (t' : 1 <= 4) by lra.
  destruct (pre_sin_bound 1 0 (Rlt_le _ _ Rlt_0_1) t') as [t _].
  apply Rlt_le_trans with (2 := t); clear t.
- simpl plus; replace (sin_approx 1 1) with (5/6);[fourier | ].
+ simpl plus; replace (sin_approx 1 1) with (5/6);[lra | ].
  unfold sin_approx, sin_term; simpl; field.
 apply sin_increasing_1.
-    assert (t := PI2_1); fourier.
+    assert (t := PI2_1); lra.
    apply Rlt_le, PI2_1.
-  assert (t := PI2_1); fourier.
- fourier.
+  assert (t := PI2_1); lra.
+ lra.
 assumption.
 Qed.
 
@@ -547,7 +547,7 @@ intros x h; rewrite Ropp_div; apply Ropp_lt_contravar; assumption.
 Qed.
 
 Lemma pos_opp_lt : forall x, 0 < x -> -x < x.
-Proof. intros; fourier. Qed.
+Proof. intros; lra. Qed.
 
 Lemma tech_opp_tan : forall x y, -tan x < y -> tan (-x) < y.
 Proof.
@@ -562,7 +562,7 @@ set (pr := (conj (tech_opp_tan _ _ (proj2 (Rabs_def2 _ _ Ptan_ub)))
 destruct (exists_atan_in_frame (-ub) ub y (pos_opp_lt _ ub0) (ub_opp _ ubpi2)
              ubpi2 pr) as [v [[vl vu] vq]].
 exists v; clear pr.
-split;[rewrite Ropp_div; split; fourier | assumption].
+split;[rewrite Ropp_div; split; lra | assumption].
 Qed.
 
 Definition atan x := let (v, _) := pre_atan x in v.
@@ -581,7 +581,7 @@ Lemma atan_opp : forall x, atan (- x) = - atan x.
 Proof.
 intros x; generalize (atan_bound (-x)); rewrite Ropp_div;intros [a b].
 generalize (atan_bound x); rewrite Ropp_div; intros [c d].
-apply tan_is_inj; try rewrite Ropp_div; try split; try fourier.
+apply tan_is_inj; try rewrite Ropp_div; try split; try lra.
 rewrite tan_neg, !atan_right_inv; reflexivity.
 Qed.
 
@@ -604,23 +604,23 @@ assert (int_tan : forall y, tan (- ub) <= y -> y <= tan ub ->
    rewrite <- (atan_right_inv y); apply tan_increasing.
      destruct (atan_bound y); assumption.
     assumption.
-   fourier.
-  fourier.
+   lra.
+  lra.
  destruct (Rle_lt_dec (atan y) ub) as [h | abs]; auto.
   assert (tan ub < y).
    rewrite <- (atan_right_inv y); apply tan_increasing.
-    rewrite Ropp_div; fourier.
+    rewrite Ropp_div; lra.
    assumption.
   destruct (atan_bound y); assumption.
- fourier.
+ lra.
 assert (incr : forall x y, -ub <= x -> x < y -> y <= ub -> tan x < tan y).
  intros y z l yz u; apply tan_increasing.
-   rewrite Ropp_div; fourier.
+   rewrite Ropp_div; lra.
   assumption.
- fourier.
+ lra.
 assert (der : forall a, -ub <= a <= ub -> derivable_pt tan a).
  intros a [la ua]; apply derivable_pt_tan.
- rewrite Ropp_div; split; fourier.
+ rewrite Ropp_div; split; lra.
 assert (df_neq : derive_pt tan (atan x)
      (derivable_pt_recip_interv_prelim1 tan atan 
         (- ub) ub x lb_lt_ub xint inv_p int_tan incr der) <> 0).
@@ -651,7 +651,7 @@ Qed.
 Lemma atan_0 : atan 0 = 0.
 Proof.
 apply tan_is_inj; try (apply atan_bound).
- assert (t := PI_RGT_0); rewrite Ropp_div; split; fourier.
+ assert (t := PI_RGT_0); rewrite Ropp_div; split; lra.
 rewrite atan_right_inv, tan_0.
 reflexivity.
 Qed.
@@ -659,7 +659,7 @@ Qed.
 Lemma atan_1 : atan 1 = PI/4.
 Proof.
 assert (ut := PI_RGT_0).
-assert (-PI/2 < PI/4 < PI/2) by (rewrite Ropp_div; split; fourier).
+assert (-PI/2 < PI/4 < PI/2) by (rewrite Ropp_div; split; lra).
 assert (t := atan_bound 1).
 apply tan_is_inj; auto.
 rewrite tan_PI4, atan_right_inv; reflexivity.
@@ -688,23 +688,23 @@ assert (int_tan : forall y, tan (- ub) <= y -> y <= tan ub ->
    rewrite <- (atan_right_inv y); apply tan_increasing.
      destruct (atan_bound y); assumption.
     assumption.
-   fourier.
-  fourier.
+   lra.
+  lra.
  destruct (Rle_lt_dec (atan y) ub) as [h | abs]; auto.
   assert (tan ub < y).
    rewrite <- (atan_right_inv y); apply tan_increasing.
-    rewrite Ropp_div; fourier.
+    rewrite Ropp_div; lra.
    assumption.
   destruct (atan_bound y); assumption.
- fourier.
+ lra.
 assert (incr : forall x y, -ub <= x -> x < y -> y <= ub -> tan x < tan y).
  intros y z l yz u; apply tan_increasing.
-   rewrite Ropp_div; fourier.
+   rewrite Ropp_div; lra.
   assumption.
- fourier.
+ lra.
 assert (der : forall a, -ub <= a <= ub -> derivable_pt tan a).
  intros a [la ua]; apply derivable_pt_tan.
- rewrite Ropp_div; split; fourier.
+ rewrite Ropp_div; split; lra.
 assert (df_neq : derive_pt tan (atan x)
      (derivable_pt_recip_interv_prelim1 tan atan 
         (- ub) ub x lb_lt_ub xint inv_p int_tan incr der) <> 0).
@@ -883,7 +883,7 @@ Proof.
 destruct (Rle_lt_dec 0 x).
  assert (pr : 0 <= x <= 1) by tauto.
  exact (ps_atan_exists_01 x pr).
-assert (pr : 0 <= -x <= 1) by (destruct Hx; split; fourier).
+assert (pr : 0 <= -x <= 1) by (destruct Hx; split; lra).
 destruct (ps_atan_exists_01 _ pr) as [v Pv].
 exists (-v).
  apply (Un_cv_ext (fun n => (- 1) * sum_f_R0 (tg_alt (Ratan_seq (- x))) n)).
@@ -898,8 +898,8 @@ Proof.
 destruct (Rle_lt_dec x 1).
  destruct (Rle_lt_dec (-1) x).
   left;split; auto.
- right;intros [a1 a2]; fourier.
-right;intros [a1 a2]; fourier.
+ right;intros [a1 a2]; lra.
+right;intros [a1 a2]; lra.
 Qed.
 
 Definition ps_atan (x : R) : R :=
@@ -922,7 +922,7 @@ unfold ps_atan.
   unfold Rdiv; rewrite !Rmult_0_l, Rmult_0_r; reflexivity.
  intros eps ep; exists 0%nat; intros n _; unfold R_dist.
  rewrite Rminus_0_r, Rabs_pos_eq; auto with real.
-case h2; split; fourier.
+case h2; split; lra.
 Qed.
 
 Lemma ps_atan_exists_1_opp :
@@ -948,9 +948,9 @@ destruct (in_int (- x)) as [inside | outside].
  destruct (in_int x) as [ins' | outs'].
  generalize (ps_atan_exists_1_opp x inside ins').
   intros h; exact h.
- destruct inside; case outs'; split; fourier.   
+ destruct inside; case outs'; split; lra.
 destruct (in_int x) as [ins' | outs'].
- destruct outside; case ins'; split; fourier.   
+ destruct outside; case ins'; split; lra.
 apply atan_opp.
 Qed.
 
@@ -1057,7 +1057,7 @@ Proof.
 intros x n.
 assert (dif : - x ^ 2 <> 1).
 apply Rlt_not_eq; apply Rle_lt_trans with 0;[ | apply Rlt_0_1].
-assert (t := pow2_ge_0 x); fourier.
+assert (t := pow2_ge_0 x); lra.
 replace (1 + x ^ 2) with (1 - - (x ^ 2)) by ring; rewrite <- (tech3 _ n dif).
 apply sum_eq; unfold tg_alt, Datan_seq; intros i _.
 rewrite pow_mult, <- Rpow_mult_distr.
@@ -1073,7 +1073,7 @@ intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition.
  apply False_ind ; intuition.
  clear -x_encad x_pos y_pos ; induction n ; unfold Datan_seq.
  case x_pos ; clear x_pos ; intro x_pos.
- simpl ; apply Rmult_gt_0_lt_compat ; intuition. fourier.
+ simpl ; apply Rmult_gt_0_lt_compat ; intuition. lra.
  rewrite x_pos ; rewrite pow_i. replace (y ^ (2*1)) with (y*y).
  apply Rmult_gt_0_compat ; assumption.
  simpl ; field.
@@ -1084,7 +1084,7 @@ intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition.
  case x_pos ; clear x_pos ; intro x_pos.
  rewrite Hrew ; rewrite Hrew.
  apply Rmult_gt_0_lt_compat ; intuition.
- apply Rmult_gt_0_lt_compat ; intuition ; fourier.
+ apply Rmult_gt_0_lt_compat ; intuition ; lra.
  rewrite x_pos.
  rewrite pow_i ; intuition.
 Qed.
@@ -1141,7 +1141,7 @@ elim (pow_lt_1_zero _ x_ub2 _ eps'_pos) ; intros N HN ; exists N.
 intros n Hn.
 assert (H1 : - x^2 <> 1).
  apply Rlt_not_eq; apply Rle_lt_trans with (2 := Rlt_0_1).
-assert (t := pow2_ge_0 x); fourier.
+assert (t := pow2_ge_0 x); lra.
 rewrite Datan_sum_eq. 
 unfold R_dist.
 assert (tool : forall a b, a / b - /b = (-1 + a) /b).
@@ -1179,13 +1179,13 @@ apply (Alt_CVU (fun x n => Datan_seq n x)
          (Datan_seq (Rabs c + r)) c r).
      intros x inb; apply Datan_seq_decreasing;
       try (apply Boule_lt in inb; apply Rabs_def2 in inb;
-         destruct inb; fourier).
+         destruct inb; lra).
     intros x inb; apply Datan_seq_CV_0;
       try (apply Boule_lt in inb; apply Rabs_def2 in inb;
-         destruct inb; fourier).
+         destruct inb; lra).
    intros x inb; apply (Datan_lim x);
       try (apply Boule_lt in inb; apply Rabs_def2 in inb;
-         destruct inb; fourier).
+         destruct inb; lra).
   intros x [ | n] inb.
    solve[unfold Datan_seq; apply Rle_refl].
   rewrite <- (Datan_seq_Rabs x); apply Rlt_le, Datan_seq_increasing.
@@ -1193,7 +1193,7 @@ apply (Alt_CVU (fun x n => Datan_seq n x)
   apply Boule_lt in inb; intuition.
   solve[apply Rabs_pos].
  apply Datan_seq_CV_0.
-  apply Rlt_trans with 0;[fourier | ].
+  apply Rlt_trans with 0;[lra | ].
   apply Rplus_le_lt_0_compat.
    solve[apply Rabs_pos].
   destruct r; assumption.
@@ -1226,7 +1226,7 @@ intros N x x_lb x_ub.
     apply Hdelta ; assumption.
     unfold id ; field ; assumption.
   intros eps eps_pos.
-  assert (eps_3_pos : (eps/3) > 0) by fourier.
+  assert (eps_3_pos : (eps/3) > 0) by lra.
   elim (IHN (eps/3) eps_3_pos) ; intros delta1 Hdelta1.
   assert (Main : derivable_pt_lim (fun x : R =>tg_alt (Ratan_seq x) (S N)) x ((tg_alt (Datan_seq x)) (S N))).
    clear -Tool ; intros eps' eps'_pos.
@@ -1297,7 +1297,7 @@ intros N x x_lb x_ub.
    intuition ; apply Rlt_le_trans with (r2:=delta) ; intuition unfold delta, mydelta.
    apply Rmin_l.
    apply Rmin_r.
-   fourier.
+   lra.
 Qed.
 
 Lemma Ratan_CVU' :
@@ -1310,7 +1310,7 @@ apply (Alt_CVU (fun i r => Ratan_seq r i) ps_atan PI_tg (/2) pos_half);
    now intros; apply Ratan_seq_converging, Boule_half_to_interval.
   intros x b; apply Boule_half_to_interval in b.
   unfold ps_atan; destruct (in_int x) as [inside | outside];
-   [ | destruct b; case outside; split; fourier].
+   [ | destruct b; case outside; split; lra].
   destruct (ps_atan_exists_1 x inside) as [v Pv].
   apply Un_cv_ext with (2 := Pv);[reflexivity].
  intros x n b; apply Boule_half_to_interval in b.
@@ -1330,7 +1330,7 @@ exists N; intros n x nN b_y.
 case (Rtotal_order 0 x) as [xgt0 | [x0 | x0]].
   assert (Boule (/2) {| pos := / 2; cond_pos := pos_half_prf|} x).
    revert b_y; unfold Boule; simpl; intros b_y; apply Rabs_def2 in b_y.
-   destruct b_y; unfold Boule; simpl; apply Rabs_def1; fourier.
+   destruct b_y; unfold Boule; simpl; apply Rabs_def1; lra.
   apply Pn; assumption.
  rewrite <- x0, ps_atan0_0.
  rewrite <- (sum_eq (fun _ => 0)), sum_cte, Rmult_0_l, Rminus_0_r, Rabs_pos_eq.
@@ -1343,7 +1343,7 @@ replace (ps_atan x - sum_f_R0 (tg_alt (Ratan_seq x)) n) with
  rewrite Rabs_Ropp.
  assert (Boule (/2) {| pos := / 2; cond_pos := pos_half_prf|} (-x)).
   revert b_y; unfold Boule; simpl; intros b_y; apply Rabs_def2 in b_y.
-  destruct b_y; unfold Boule; simpl; apply Rabs_def1; fourier.
+  destruct b_y; unfold Boule; simpl; apply Rabs_def1; lra.
  apply Pn; assumption.
 unfold Rminus; rewrite ps_atan_opp, Ropp_plus_distr, sum_Ratan_seq_opp.
 rewrite !Ropp_involutive; reflexivity.
@@ -1372,7 +1372,7 @@ apply continuity_inv.
 apply continuity_plus.
 apply continuity_const ; unfold constant ; intuition.
 apply derivable_continuous ; apply derivable_pow.
-intro x ; apply Rgt_not_eq ; apply Rge_gt_trans with (1+0) ; [|fourier] ;
+intro x ; apply Rgt_not_eq ; apply Rge_gt_trans with (1+0) ; [|lra] ;
  apply Rplus_ge_compat_l.
  replace (x^2) with (x²).
  apply Rle_ge ; apply Rle_0_sqr.
@@ -1393,11 +1393,11 @@ apply derivable_pt_lim_CVU with
     assumption.
    intros y N inb; apply Rabs_def2 in inb; destruct inb.
    apply Datan_is_datan.
-    fourier.
-   fourier.
+    lra.
+   lra.
   intros y inb; apply Rabs_def2 in inb; destruct inb.
-  assert (y_gt_0 : -1 < y) by fourier.
-  assert (y_lt_1 : y < 1) by fourier.
+  assert (y_gt_0 : -1 < y) by lra.
+  assert (y_lt_1 : y < 1) by lra.
   intros eps eps_pos ; elim (Ratan_is_ps_atan eps eps_pos).
   intros N HN ; exists N; intros n n_lb ; apply HN ; tauto.
  apply Datan_CVU_prelim.
@@ -1406,8 +1406,8 @@ apply derivable_pt_lim_CVU with
  replace ((c + r - (c - r)) / 2) with (r :R) by field.
  assert (Rabs c < 1 - r).
   unfold Boule in Pcr1; destruct r; simpl in *; apply Rabs_def1;
-  apply Rabs_def2 in Pcr1; destruct Pcr1; fourier.
- fourier.
+  apply Rabs_def2 in Pcr1; destruct Pcr1; lra.
+ lra.
 intros; apply Datan_continuity.
 Qed.
 
@@ -1426,7 +1426,7 @@ Lemma ps_atan_continuity_pt_1 : forall eps : R,
        dist R_met (ps_atan x) (Alt_PI/4) < eps).
 Proof.
 intros eps eps_pos.
-assert (eps_3_pos : eps / 3 > 0) by fourier.
+assert (eps_3_pos : eps / 3 > 0) by lra.
 elim (Ratan_is_ps_atan (eps / 3) eps_3_pos) ; intros N1 HN1.
 unfold Alt_PI.
 destruct exist_PI as [v Pv]; replace ((4 * v)/4) with v by field.
@@ -1461,10 +1461,10 @@ rewrite Rplus_assoc ; apply Rabs_triang.
    unfold D_x, no_cond ; split ; [ | apply Rgt_not_eq ] ; intuition.
    intuition.
    apply HN2; unfold N; omega.
-   fourier.
+   lra.
   rewrite <- Rabs_Ropp, Ropp_minus_distr; apply HN1.
      unfold N; omega.  
-    fourier.
+    lra.
   assumption.
  field.
 ring.
@@ -1486,11 +1486,11 @@ intros x x_encad Pratan Prmymeta.
   rewrite Hrew1.
   replace (Rsqr x) with (x ^ 2) by (unfold Rsqr; ring).
   unfold Rdiv; rewrite Rmult_1_l; reflexivity.
-     fourier.
+     lra.
     assumption.
    intros; reflexivity.
-  fourier.
- assert (t := tan_1_gt_1); split;destruct x_encad; fourier.
+  lra.
+ assert (t := tan_1_gt_1); split;destruct x_encad; lra.
 intros; reflexivity.
 Qed.
 
@@ -1503,46 +1503,46 @@ assert (pr1 : forall c : R, 0 < c < x -> derivable_pt (atan - ps_atan) c).
  apply derivable_pt_minus.
   exact (derivable_pt_atan c).
  apply derivable_pt_ps_atan.
-  destruct x_encad; destruct c_encad; split; fourier.
+  destruct x_encad; destruct c_encad; split; lra.
 assert (pr2 : forall c : R, 0 < c < x -> derivable_pt id c).
- intros ; apply derivable_pt_id; fourier.
+ intros ; apply derivable_pt_id; lra.
 assert (delta_cont : forall c : R, 0 <= c <= x -> continuity_pt (atan - ps_atan) c).
  intros c [[c_encad1 | c_encad1 ] [c_encad2 | c_encad2]];
         apply continuity_pt_minus.
         apply derivable_continuous_pt ; apply derivable_pt_atan. 
        apply derivable_continuous_pt ; apply derivable_pt_ps_atan.
-       split; destruct x_encad; fourier.
+       split; destruct x_encad; lra.
       apply derivable_continuous_pt, derivable_pt_atan.
      apply derivable_continuous_pt, derivable_pt_ps_atan.
-     subst c; destruct x_encad; split; fourier.
+     subst c; destruct x_encad; split; lra.
     apply derivable_continuous_pt, derivable_pt_atan.
    apply derivable_continuous_pt, derivable_pt_ps_atan.
-   subst c; split; fourier.
+   subst c; split; lra.
   apply derivable_continuous_pt, derivable_pt_atan.
  apply derivable_continuous_pt, derivable_pt_ps_atan.
- subst c; destruct x_encad; split; fourier.
+ subst c; destruct x_encad; split; lra.
 assert (id_cont : forall c : R, 0 <= c <= x -> continuity_pt id c).
     intros ; apply derivable_continuous ; apply derivable_id.
-assert (x_lb : 0 < x) by (destruct x_encad; fourier).
+assert (x_lb : 0 < x) by (destruct x_encad; lra).
 elim (MVT (atan - ps_atan)%F id 0 x pr1 pr2 x_lb delta_cont id_cont) ; intros d Temp ; elim Temp ; intros d_encad Main.
 clear - Main x_encad.
 assert (Temp : forall (pr: derivable_pt (atan - ps_atan) d), derive_pt (atan - ps_atan) d pr = 0).
  intro pr.
  assert (d_encad3 : -1 < d < 1).
-  destruct d_encad; destruct x_encad; split; fourier.
+  destruct d_encad; destruct x_encad; split; lra.
  pose (pr3 := derivable_pt_minus atan ps_atan d (derivable_pt_atan d) (derivable_pt_ps_atan d d_encad3)).
  rewrite <- pr_nu_var2_interv with (f:=(atan - ps_atan)%F) (g:=(atan - ps_atan)%F) (lb:=0) (ub:=x) (pr1:=pr3) (pr2:=pr).
     unfold pr3. rewrite derive_pt_minus.
     rewrite Datan_eq_DatanSeq_interv with (Prmymeta := derivable_pt_atan d).
      intuition.
     assumption. 
-   destruct d_encad; fourier.
+   destruct d_encad; lra.
   assumption.
  reflexivity.
 assert (iatan0 : atan 0 = 0).
  apply tan_is_inj.
    apply atan_bound.
-  rewrite Ropp_div; assert (t := PI2_RGT_0); split; fourier.
+  rewrite Ropp_div; assert (t := PI2_RGT_0); split; lra.
  rewrite tan_0, atan_right_inv; reflexivity.
 generalize Main; rewrite Temp, Rmult_0_r.
 replace ((atan - ps_atan)%F x) with (atan x - ps_atan x) by intuition.
@@ -1560,19 +1560,19 @@ Qed.
 Theorem Alt_PI_eq : Alt_PI = PI.
 Proof.
 apply Rmult_eq_reg_r with (/4); fold (Alt_PI/4); fold (PI/4);
-  [ | apply Rgt_not_eq; fourier].
+  [ | apply Rgt_not_eq; lra].
 assert (0 < PI/6) by (apply PI6_RGT_0).
 assert (t1:= PI2_1).
 assert (t2 := PI_4).
 assert (m := Alt_PI_RGT_0).
-assert (-PI/2 < 1 < PI/2) by (rewrite Ropp_div; split; fourier).
+assert (-PI/2 < 1 < PI/2) by (rewrite Ropp_div; split; lra).
 apply cond_eq; intros eps ep.
 change (R_dist (Alt_PI/4) (PI/4) < eps).
 assert (ca : continuity_pt atan 1).
   apply derivable_continuous_pt, derivable_pt_atan.
 assert (Xe : exists eps', exists eps'',
   eps' + eps'' <= eps /\ 0 < eps' /\ 0 < eps'').
- exists (eps/2); exists (eps/2); repeat apply conj; fourier.
+ exists (eps/2); exists (eps/2); repeat apply conj; lra.
 destruct Xe as [eps' [eps'' [eps_ineq [ep' ep'']]]].
 destruct (ps_atan_continuity_pt_1 _ ep') as [alpha [a0 Palpha]].
 destruct (ca _ ep'') as [beta [b0 Pbeta]].
@@ -1585,14 +1585,14 @@ assert (Xa : exists a, 0 < a < 1 /\ R_dist a 1 < alpha /\
  assert ((1 - alpha /2) <= Rmax (1 - alpha /2) (1 - beta /2)) by apply Rmax_l.
  assert ((1 - beta /2) <= Rmax (1 - alpha /2) (1 - beta /2)) by apply Rmax_r.
  assert (Rmax (1 - alpha /2) (1 - beta /2) < 1)
-   by (apply Rmax_lub_lt; fourier).
- split;[split;[ | apply Rmax_lub_lt]; fourier | ].
+   by (apply Rmax_lub_lt; lra).
+ split;[split;[ | apply Rmax_lub_lt]; lra | ].
  assert (0 <= 1 - Rmax (/ 2) (Rmax (1 - alpha / 2) (1 - beta / 2))).
   assert (Rmax (/2) (Rmax (1 - alpha / 2) 
-            (1 - beta /2)) <= 1) by (apply Rmax_lub; fourier).
-  fourier.
+            (1 - beta /2)) <= 1) by (apply Rmax_lub; lra).
+  lra.
  split; unfold R_dist; rewrite <-Rabs_Ropp, Ropp_minus_distr,
-   Rabs_pos_eq;fourier.
+   Rabs_pos_eq;lra.
 destruct Xa as [a [[Pa0 Pa1] [P1 P2]]].
 apply Rle_lt_trans with (1 := R_dist_tri _ _ (ps_atan a)).
 apply Rlt_le_trans with (2 := eps_ineq).
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index aa886cee0..59e014862 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -15,7 +15,7 @@
 
 Require Import Rbase.
 Require Import R_Ifp.
-Require Import Fourier.
+Require Import Lra.
 Local Open Scope R_scope.
 
 Implicit Type r : R.
@@ -357,7 +357,7 @@ Qed.
 
 Lemma Rle_abs : forall x:R, x <= Rabs x.
 Proof.
-  intro; unfold Rabs; case (Rcase_abs x); intros; fourier.
+  intro; unfold Rabs; case (Rcase_abs x); intros; lra.
 Qed.
 
 Definition RRle_abs := Rle_abs.
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index dfa5c7104..aaf691ed1 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.v
@@ -16,7 +16,7 @@
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rlimit.
-Require Import Fourier.
+Require Import Lra.
 Require Import Omega.
 Local Open Scope R_scope.
 
@@ -77,7 +77,7 @@ Proof.
   elim (Rmin_Rgt (/ 2) x 0); intros a b; cut (0 < 2).
   intro; generalize (Rinv_0_lt_compat 2 H3); intro; fold (/ 2 > 0) in H4;
     apply (b (conj H4 H)).
-  fourier.
+  lra.
   intros; elim H3; clear H3; intros;
     generalize
       (let (H1, H2) :=
@@ -167,7 +167,7 @@ Proof.
   unfold Rabs; destruct (Rcase_abs 2) as [Hlt|Hge]; auto.
   cut (0 < 2).
   intro H7; elim (Rlt_asym 0 2 H7 Hlt).
-  fourier.
+  lra.
   apply Rabs_no_R0.
   discrR.
 Qed.
diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v
index b249b519f..3ef368bb4 100644
--- a/theories/Reals/Reals.v
+++ b/theories/Reals/Reals.v
@@ -30,3 +30,4 @@ Require Export SeqSeries.
 Require Export Rtrigo.
 Require Export Ranalysis.
 Require Export Integration.
+Require Import Fourier.
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index b14fcc4d3..e3e995d20 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -15,7 +15,7 @@
 
 Require Import Rbase.
 Require Import Rfunctions.
-Require Import Fourier.
+Require Import Lra.
 Local Open Scope R_scope.
 
 (*******************************)
@@ -24,7 +24,7 @@ Local Open Scope R_scope.
 (*********)
 Lemma eps2_Rgt_R0 : forall eps:R, eps > 0 -> eps * / 2 > 0.
 Proof.
-  intros; fourier.
+  intros; lra.
 Qed.
 
 (*********)
@@ -45,14 +45,14 @@ Qed.
 Lemma Rlt_eps2_eps : forall eps:R, eps > 0 -> eps * / 2 < eps.
 Proof.
   intros.
-  fourier.
+  lra.
 Qed.
 
 (*********)
 Lemma Rlt_eps4_eps : forall eps:R, eps > 0 -> eps * / (2 + 2) < eps.
 Proof.
   intros.
-  fourier.
+  lra.
 Qed.
 
 (*********)
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index c6fac951b..d465523a7 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -25,7 +25,7 @@ Require Import R_sqrt.
 Require Import Sqrt_reg.
 Require Import MVT.
 Require Import Ranalysis4.
-Require Import Fourier.
+Require Import Lra.
 Local Open Scope R_scope.
 
 Lemma P_Rmin : forall (P:R -> Prop) (x y:R), P x -> P y -> P (Rmin x y).
@@ -714,7 +714,7 @@ Qed.
 Lemma Rlt_Rpower_l a b c: 0 < c -> 0 < a < b -> a ^R c < b ^R c.
 Proof.
 intros c0 [a0 ab]; apply exp_increasing.
-now apply Rmult_lt_compat_l; auto; apply ln_increasing; fourier.
+now apply Rmult_lt_compat_l; auto; apply ln_increasing; lra.
 Qed.
 
 Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> a ^R c <= b ^R c.
@@ -722,7 +722,7 @@ Proof.
 intros [c0 | c0];
  [ | intros; rewrite <- c0, !Rpower_O; [apply Rle_refl | |] ].
   intros [a0 [ab|ab]].
-  now apply Rlt_le, Rlt_Rpower_l;[ | split]; fourier.
+  now apply Rlt_le, Rlt_Rpower_l;[ | split]; lra.
   rewrite ab; apply Rle_refl.
  apply Rlt_le_trans with a; tauto.
 tauto.
@@ -754,10 +754,10 @@ assert (cmp : 0 < x + sqrt (x ^ 2 + 1)).
   replace (x ^ 2) with ((-x) ^ 2) by ring.
   assert (sqrt ((- x) ^ 2) < sqrt ((-x)^2+1)).
    apply sqrt_lt_1_alt.
-   split;[apply pow_le | ]; fourier.
+   split;[apply pow_le | ]; lra.
   pattern x at 1; replace x with (- (sqrt ((- x) ^ 2))).
-   assert (t:= sqrt_pos ((-x)^2)); fourier.
-  simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive;[reflexivity | fourier].
+   assert (t:= sqrt_pos ((-x)^2)); lra.
+  simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive;[reflexivity | lra].
   apply Rplus_lt_le_0_compat;[apply Rnot_le_gt; assumption | apply sqrt_pos].
 rewrite exp_ln;[ | assumption].
 rewrite exp_Ropp, exp_ln;[ | assumption].
@@ -770,7 +770,7 @@ apply Rmult_eq_reg_l with (2 * (x + sqrt (x ^ 2 + 1)));[ |
  apply Rgt_not_eq, Rmult_lt_0_compat;[apply Rlt_0_2 | assumption]].
 assert (pow2_sqrt : forall x, 0 <= x -> sqrt x ^ 2 = x) by
  (intros; simpl; rewrite Rmult_1_r, sqrt_sqrt; auto).
-field_simplify;[rewrite pow2_sqrt;[field | ] | apply Rgt_not_eq; fourier].
+field_simplify;[rewrite pow2_sqrt;[field | ] | apply Rgt_not_eq; lra].
 apply Rplus_le_le_0_compat;[simpl; rewrite Rmult_1_r; apply (Rle_0_sqr x)|apply Rlt_le, Rlt_0_1].
 Qed.
 
@@ -784,12 +784,12 @@ assert (0 < x + sqrt (x ^ 2 + 1)).
  replace (x ^ 2) with ((-x) ^ 2) by ring.
  assert (sqrt ((- x) ^ 2) < sqrt ((-x)^2+1)).
   apply sqrt_lt_1_alt.
-  split;[apply pow_le|]; fourier.
+  split;[apply pow_le|]; lra.
  pattern x at 1; replace x with (- (sqrt ((- x) ^ 2))).
-  assert (t:= sqrt_pos ((-x)^2)); fourier.
- simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive; auto; fourier.
+  assert (t:= sqrt_pos ((-x)^2)); lra.
+ simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive; auto; lra.
 assert (0 < x ^ 2 + 1).
- apply Rplus_le_lt_0_compat;[simpl; rewrite Rmult_1_r; apply Rle_0_sqr|fourier].
+ apply Rplus_le_lt_0_compat;[simpl; rewrite Rmult_1_r; apply Rle_0_sqr|lra].
 replace (/sqrt (x ^ 2 + 1)) with
  (/(x + sqrt (x ^ 2 + 1)) * 
     (1 + (/(2 * sqrt (x ^ 2 + 1)) * (INR 2 * x ^ 1 + 0)))).
@@ -817,7 +817,7 @@ intros x y xy.
 case (Rle_dec (arcsinh y) (arcsinh x));[ | apply Rnot_le_lt ].
 intros abs; case (Rlt_not_le _ _ xy).
 rewrite <- (sinh_arcsinh y), <- (sinh_arcsinh x).
-destruct abs as [lt | q];[| rewrite q; fourier].
+destruct abs as [lt | q];[| rewrite q; lra].
 apply Rlt_le, sinh_lt; assumption.
 Qed.
 
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index ffc0adf50..ddd8722e1 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -18,7 +18,7 @@ Require Export Cos_rel.
 Require Export Cos_plus.
 Require Import ZArith_base.
 Require Import Zcomplements.
-Require Import Fourier.
+Require Import Lra.
 Require Import Ranalysis1.
 Require Import Rsqrt_def. 
 Require Import PSeries_reg.
diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v
index bf00f736f..a75fd2dde 100644
--- a/theories/Reals/Rtrigo1.v
+++ b/theories/Reals/Rtrigo1.v
@@ -18,7 +18,7 @@ Require Export Cos_rel.
 Require Export Cos_plus.
 Require Import ZArith_base.
 Require Import Zcomplements.
-Require Import Fourier.
+Require Import Lra.
 Require Import Ranalysis1.
 Require Import Rsqrt_def. 
 Require Import PSeries_reg.
@@ -175,10 +175,10 @@ 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.
+assert (lo1 : 0 <= 7/8) by lra.
+assert (up1 : 7/8 <= 4) by lra.
+assert (lo : -2 <= 7/8) by lra.
+assert (up : 7/8 <= 2) by lra.
 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).
@@ -205,12 +205,12 @@ 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).
+ assert (int78 : -2 <= 7/8 <= 2) by (split; lra).
  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.
+ lra.
 assert (cun : cos (7/4) < 0).
  replace (7/4) with (7/8 + 7/8) by field.
  rewrite cos_plus.
@@ -218,7 +218,7 @@ assert (cun : cos (7/4) < 0).
    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.
+apply IVT; auto; lra.
 Qed.
 
 Definition PI2 := proj1_sig PI_2_aux.
@@ -270,7 +270,7 @@ 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).
+assert (up : x <= 4) by (apply Rlt_le, Rlt_trans with (1:=int2); lra).
 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.
@@ -280,13 +280,13 @@ 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 ].
+apply Rmult_lt_0_compat;[assumption | lra ].
 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.
+ destruct pi2_int; split; lra.
 assert (lo2 := sin_pos_tech PI2 int').
 assert (t2 : Rabs (sin PI2) = 1).
  rewrite <- Rabs_R1; apply Rsqr_eq_abs_0.
@@ -295,10 +295,10 @@ 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.
+Proof. unfold PI; destruct pi2_int; lra. Qed.
 
 Lemma PI_4 : PI <= 4.
-Proof. unfold PI; destruct pi2_int; fourier. Qed.
+Proof. unfold PI; destruct pi2_int; lra. Qed.
 
 (**********)
 Lemma PI_neq0 : PI <> 0.
@@ -344,13 +344,13 @@ Lemma cos_bound : forall (a : R) (n : nat), - PI / 2 <= a -> a <= PI / 2 ->
 Proof.
 intros a n lower upper; apply pre_cos_bound.
  apply Rle_trans with (2 := lower).
- apply Rmult_le_reg_r with 2; [fourier |].
+ apply Rmult_le_reg_r with 2; [lra |].
  replace ((-PI/2) * 2) with (-PI) by field.
- assert (t := PI_4); fourier.
+ assert (t := PI_4); lra.
 apply Rle_trans with (1 := upper).
-apply Rmult_le_reg_r with 2; [fourier | ].
+apply Rmult_le_reg_r with 2; [lra | ].
 replace ((PI/2) * 2) with PI by field.
-generalize PI_4; intros; fourier.
+generalize PI_4; intros; lra.
 Qed.
 (**********)
 Lemma neg_cos : forall x:R, cos (x + PI) = - cos x.
@@ -749,19 +749,19 @@ Qed.
 Lemma _PI2_RLT_0 : - (PI / 2) < 0.
 Proof.
   assert (H := PI_RGT_0).
-  fourier.
+  lra.
 Qed.
 
 Lemma PI4_RLT_PI2 : PI / 4 < PI / 2.
 Proof.
   assert (H := PI_RGT_0).
-  fourier.
+  lra.
 Qed.
 
 Lemma PI2_Rlt_PI : PI / 2 < PI.
 Proof.
   assert (H := PI_RGT_0).
-  fourier.
+  lra.
 Qed.
 
 (***************************************************)
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v
index 7cbfc6303..78797c87c 100644
--- a/theories/Reals/Rtrigo_calc.v
+++ b/theories/Reals/Rtrigo_calc.v
@@ -205,7 +205,6 @@ Proof with trivial.
   rewrite cos2; unfold Rsqr; rewrite sin_PI6; rewrite sqrt_def...
   field.
   left ; prove_sup0.
-  discrR.
 Qed.
 
 Lemma tan_PI6 : tan (PI / 6) = 1 / sqrt 3.
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index c640167ac..05bc6aea9 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -76,7 +76,7 @@ let is_tactic =
     [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
       "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; 
       "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
-      "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto";
+      "info"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto";
       "quote"; "eexact"; "autorewrite";
       "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
       "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";