Remove fourier plugin

As stated in the manual, the fourier tactic is subsumed by lra.

13 files changed, 257 insertions, 242 deletions

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.