diff --git a/examples/Cody_Waite.v b/examples/Cody_Waite.v
index dee51f9a7e265fa3328e5c9f1b168f9e84783495..f6b02871dc23d63f9d0e5702817f96587b8d9e00 100644
--- a/examples/Cody_Waite.v
+++ b/examples/Cody_Waite.v
@@ -1,4 +1,4 @@
-Require Import Reals Flocq.Core.Fcore.
+Require Import Reals Flocq.Core.Core.
 Require Import Gappa.Gappa_tactic Interval.Interval_tactic.
 
 Open Scope R_scope.
@@ -74,7 +74,7 @@ Lemma method_error :
   Rabs ((f - exp t) / exp t) <= 23 * pow2 (-62).
 Proof.
 intros t t2 p q f Ht.
-unfold f, q, p, t2, p0, p1, p2, q0, q1, q2 ; simpl ;
+unfold f, q, p, t2, p0, p1, p2, q0, q1, q2 ;
 interval with (i_bisect_taylor t 9, i_prec 70).
 Qed.
 
@@ -103,11 +103,11 @@ assert (Rabs x <= 5/16 \/ 5/16 <= Rabs x <= 746) as [Bx'|Bx'] by gappa.
   rewrite 2!round_generic with (2 := Fx)...
   gappa.
 - assert (Hl: - 1 * pow2 (-102) <= Log2l - (ln 2 - Log2h) <= 0).
-    unfold Log2l, Log2h ; simpl bpow ;
+    unfold Log2l, Log2h ;
     interval with (i_prec 110).
   assert (Ax: x = x * InvLog2 * (1 / InvLog2)).
     field.
-    unfold InvLog2 ; simpl ; interval.
+    unfold InvLog2 ; interval.
   unfold te.
   replace (x - k * ln 2) with (x - k * Log2h - k * (ln 2 - Log2h)) by ring.
   revert Hl Ax.
@@ -152,9 +152,9 @@ assert (Rabs ((exp t - exp x) / exp x) <= 33 * pow2 (-60)).
   rewrite <- exp_Ropp, <- exp_plus.
   revert Ex.
   unfold Rminus ; generalize (t + - x) ; clear.
-  simpl ; intros r Hr ; interval with (i_prec 60).
+  intros r Hr ; interval with (i_prec 60).
 apply rel_helper. apply Rgt_not_eq, exp_pos.
 apply rel_helper in H. 2: apply Rgt_not_eq, exp_pos.
 apply rel_helper in Ef. 2: apply Rgt_not_eq, exp_pos.
-unfold t2, add, mul, sub, div, p0, p1, p2, q0, q1, q2 in * ; simpl bpow in * ; gappa.
+unfold t2, add, mul, sub, div, p0, p1, p2, q0, q1, q2 in * ; gappa.
 Qed.
diff --git a/examples/Division_u16.v b/examples/Division_u16.v
index f74ec270e6fdc679a8b51ad01c43ee566ae9b683..8811408b9aeb909b48b1b0be6e9495f8f775c761 100644
--- a/examples/Division_u16.v
+++ b/examples/Division_u16.v
@@ -1,5 +1,5 @@
 Require Import Reals Psatz.
-Require Import Fcore Gappa.Gappa_tactic.
+Require Import Flocq.Core.Core Gappa.Gappa_tactic.
 
 Open Scope R_scope.
 
@@ -21,7 +21,6 @@ Lemma FIX_format_IZR :
 Proof.
 intros beta x.
 exists (Float beta x 0).
-split.
 apply sym_eq, Rmult_1_r.
 apply eq_refl.
 Qed.
@@ -106,10 +105,8 @@ cut (0 <= b * q1 - a < 1).
   generalize (Z_mod_lt a b).
   lia.
 assert (Ba': 1 <= a <= 65535).
-  change (1%Z <= a <= 65535%Z).
   now split ; apply IZR_le.
 assert (Bb': 1 <= b <= 65535).
-  change (1%Z <= b <= 65535%Z).
   now split ; apply IZR_le.
 refine (let '(conj H1 H2) := _ in conj H1 (Rnot_le_lt _ _ H2)).
 set (err := (q1 - a / b) / (a / b)).
diff --git a/examples/Sqrt_sqr.v b/examples/Sqrt_sqr.v
index ef18207f032065e18e950238d36ddbace58cb167..4a223585f2144b0e8ab3aba5874e9c2351a4e477 100644
--- a/examples/Sqrt_sqr.v
+++ b/examples/Sqrt_sqr.v
@@ -1,4 +1,5 @@
-Require Import Flocq.Core.Fcore.
+Require Import Reals Psatz.
+Require Import Flocq.Core.Core.
 Require Import Interval.Interval_tactic.
 
 Section Sec1.
@@ -117,7 +118,7 @@ right; field.
 rewrite 2!ulp_neq_0.
 2: now apply Rgt_not_eq.
 2: now apply Rgt_not_eq.
-unfold canonic_exp, FLX_exp.
+unfold cexp, FLX_exp.
 destruct (mag beta x) as (e,He).
 simpl.
 assert (bpow (e - 1) <= x < bpow e).
@@ -232,7 +233,7 @@ rewrite ulp_neq_0.
 2: apply Rmult_integral_contrapositive_currified; apply Rgt_not_eq.
 2: apply Rlt_0_2.
 2: apply bpow_gt_0.
-unfold canonic_exp, FLX_exp.
+unfold cexp, FLX_exp.
 right; apply f_equal.
 apply f_equal2; try reflexivity.
 apply sym_eq, mag_unique.
@@ -255,7 +256,6 @@ rewrite <- succ_eq_pos.
 apply succ_le_lt...
 apply generic_format_FLX.
 exists (Float beta 2 (e-1)).
-simpl; split.
 unfold F2R; now simpl.
 apply Zlt_le_trans with (4^1)%Z.
 simpl; unfold Z.pow_pos; simpl; omega.
@@ -302,7 +302,7 @@ intros u Hu.
 rewrite 2!ulp_neq_0.
 2: now apply Rgt_not_eq.
 2: now apply Rgt_not_eq, Rmult_lt_0_compat.
-unfold canonic_exp, FLX_exp.
+unfold cexp, FLX_exp.
 (* *)
 destruct (mag beta u) as (e,He); simpl.
 intros Cu.
@@ -342,6 +342,7 @@ generalize (radix_gt_0 beta); intros.
 left; now apply IZR_lt.
 rewrite H.
 apply Rlt_le_trans with (2 * bpow (e-1) * bpow (e - prec)).
+change 2%R with (1 + 1)%R.
 rewrite Rmult_assoc, Rmult_plus_distr_r, Rmult_1_l.
 rewrite <- 2!bpow_plus.
 replace (e - 1 + (e - prec))%Z with (2 * e - 1 - prec)%Z by ring.
@@ -388,8 +389,7 @@ apply Rle_trans with (ulp_flx x).
 right; field; auto with real.
 apply Rle_trans with x.
 apply ulp_le_id; auto.
-rewrite Rmult_1_r, <- (Rplus_0_l x) at 1.
-rewrite Rmult_plus_distr_l, Rmult_1_r; auto with real.
+lra.
 assert (0 <= 1 - ulp_flx (x * x) / 2 / (x * x)).
 apply Rplus_le_reg_l with (ulp_flx (x*x) / 2 / (x*x)); ring_simplify.
 apply Rmult_le_reg_l with 2; auto with real.
@@ -398,15 +398,14 @@ apply Rle_trans with (ulp_flx (x*x)).
 right; field; auto with real.
 apply Rle_trans with (x*x).
 rewrite ulp_neq_0; try now apply Rgt_not_eq.
-unfold canonic_exp, FLX_exp.
+unfold cexp, FLX_exp.
 destruct (mag beta (x*x)) as (e,He); simpl.
 apply Rle_trans with (bpow (e-1)).
 apply bpow_le; auto with zarith.
 rewrite <- (Rabs_right (x*x)).
 apply He; auto with real.
 apply Rle_ge; auto with real.
-rewrite Rmult_1_r, <- (Rplus_0_l (x*x)) at 1.
-rewrite Rmult_plus_distr_l, Rmult_1_r; auto with real.
+lra.
 assert (0 <= 1 + ulp_flx x / 2 / x).
 rewrite <- (Rplus_0_l 0).
 apply Rplus_le_compat; auto with real.
@@ -604,7 +603,7 @@ intros Hb.
 apply Rle_lt_trans with (sqrt (IZR beta) * bpow (mag beta x - 1)
     - IZR k * ulp_flx x).
 rewrite ulp_neq_0; try now apply Rgt_not_eq.
-unfold canonic_exp, FLX_exp.
+unfold cexp, FLX_exp.
 apply Rle_trans with (bpow (mag beta x - 1)
    *(sqrt (IZR beta) -IZR k * bpow (1-prec))).
 rewrite <- (Rmult_1_r (bpow (mag beta x - 1))) at 1.
@@ -705,8 +704,7 @@ Proof with auto with typeclass_instances.
 apply generic_format_FLX.
 unfold generic_format in Fx.
 exists  (Float beta (Ztrunc (scaled_mantissa beta (FLX_exp prec) x) - k)
-                    (canonic_exp beta (FLX_exp prec) x)).
-split.
+                    (cexp beta (FLX_exp prec) x)).
 unfold xk; rewrite Fx at 1; unfold F2R; simpl.
 rewrite minus_IZR; ring_simplify.
 apply f_equal.
@@ -719,14 +717,14 @@ apply Zplus_le_compat_l.
 omega.
 rewrite Zminus_0_r.
 apply lt_IZR.
-apply Rmult_lt_reg_r with (bpow (canonic_exp beta (FLX_exp prec) x)).
+apply Rmult_lt_reg_r with (bpow (cexp beta (FLX_exp prec) x)).
 apply bpow_gt_0.
 apply Rle_lt_trans with x.
 rewrite Fx at 3.
 right; unfold F2R; reflexivity.
 rewrite IZR_Zpower.
 rewrite <- bpow_plus.
-unfold canonic_exp, FLX_exp.
+unfold cexp, FLX_exp.
 replace  (prec + (mag beta x - prec))%Z with (mag beta x+0)%Z by ring.
 rewrite Zplus_0_r.
 apply Rle_lt_trans with (Rabs x).
@@ -734,7 +732,7 @@ apply RRle_abs.
 apply bpow_mag_gt...
 omega.
 apply le_IZR.
-apply Rmult_le_reg_r with (bpow (canonic_exp beta (FLX_exp prec) x)).
+apply Rmult_le_reg_r with (bpow (cexp beta (FLX_exp prec) x)).
 apply bpow_gt_0.
 rewrite Rmult_0_l.
 apply Rle_trans with xk.
@@ -770,7 +768,7 @@ unfold pred_pos; rewrite Req_bool_false.
 replace (ulp_flx xk) with (ulp_flx x).
 unfold xk; right; field.
 rewrite 2!ulp_neq_0; try apply Rgt_not_eq; try assumption.
-unfold canonic_exp; now rewrite Z.
+unfold cexp; now rewrite Z.
 apply xkpos.
 apply Rle_lt_trans with (x-(IZR k+/2)*ulp_flx x).
 right; unfold Rdiv; ring.
@@ -784,7 +782,7 @@ auto with real.
 apply ulp_ge_0.
 interval.
 rewrite ulp_neq_0; try now apply Rgt_not_eq.
-unfold canonic_exp, FLX_exp.
+unfold cexp, FLX_exp.
 apply bpow_le; omega.
 rewrite Rmult_1_l.
 left; apply xkgt.
@@ -796,7 +794,7 @@ split.
 apply Rmult_le_pos; assumption.
 apply Rlt_le_trans with (x*x - /2*bpow (2 * mag beta x  - prec)).
 rewrite ulp_neq_0; try now apply Rgt_not_eq.
-unfold canonic_exp, FLX_exp.
+unfold cexp, FLX_exp.
 apply Rplus_lt_reg_r with (-x*x).
 apply Rle_lt_trans with
   (- (bpow (mag beta x - prec)*((2*IZR k +1)*x -
@@ -828,7 +826,7 @@ apply Rmult_le_compat_l.
 left; auto with real.
 rewrite ulp_neq_0.
 2: apply Rmult_integral_contrapositive_currified; now apply Rgt_not_eq.
-unfold canonic_exp, FLX_exp.
+unfold cexp, FLX_exp.
 apply bpow_le.
 apply Zplus_le_compat_r.
 apply mag_le_bpow.
@@ -970,7 +968,7 @@ auto with real.
 apply bpow_gt_0.
 assert (bpow (mag beta x - prec)=ulp_flx (2 * bpow (mag beta x - 1))).
 rewrite ulp_neq_0; try now apply Rgt_not_eq.
-unfold canonic_exp, FLX_exp.
+unfold cexp, FLX_exp.
 apply f_equal.
 apply f_equal2; try reflexivity.
 apply sym_eq, mag_unique.
@@ -993,8 +991,7 @@ rewrite <- succ_eq_pos;[idtac|now left].
 apply succ_le_lt...
 apply generic_format_FLX.
 exists (Float beta 2 (mag beta x -1)).
-simpl; split.
-unfold F2R; simpl; ring.
+easy.
 rewrite H; apply Zlt_le_trans with (4^1)%Z.
 simpl; unfold Z.pow_pos; simpl; omega.
 apply (Zpower_le (Build_radix 4 eq_refl)).
@@ -1035,8 +1032,9 @@ apply Fourier_util.Rlt_mult_inv_pos.
 apply Rmult_lt_0_compat.
 assumption.
 apply bpow_gt_0.
-rewrite Rplus_comm, <-Rplus_assoc; apply Rle_lt_0_plus_1, Rlt_le, Rle_lt_0_plus_1.
-apply bpow_ge_0.
+apply Rplus_lt_0_compat.
+now apply IZR_lt.
+apply bpow_gt_0.
 assert (0 < Zceil (x * bpow (1 - mag beta x) / (2+bpow (1-prec))))%Z.
 apply lt_IZR.
 apply Rlt_le_trans with (1:=H).
@@ -1053,8 +1051,9 @@ apply Rle_trans with (bpow 1 / 1).
 unfold Rdiv; apply Rmult_le_compat.
 apply Rmult_le_pos; try apply bpow_ge_0; now left.
 apply Rlt_le, Rinv_0_lt_compat.
-rewrite Rplus_comm, <-Rplus_assoc; apply Rle_lt_0_plus_1, Rlt_le, Rle_lt_0_plus_1.
-apply bpow_ge_0.
+apply Rplus_lt_0_compat.
+now apply IZR_lt.
+apply bpow_gt_0.
 apply Rle_trans with (bpow (mag beta x)*bpow (1 - mag beta x)).
 apply Rmult_le_compat_r.
 apply bpow_ge_0.
@@ -1081,8 +1080,9 @@ apply Rmult_le_pos.
 now left.
 apply bpow_ge_0.
 apply Rlt_le, Rinv_0_lt_compat.
-rewrite Rplus_comm, <-Rplus_assoc.
-apply Rle_lt_0_plus_1, Rlt_le, Rle_lt_0_plus_1, bpow_ge_0.
+apply Rplus_lt_0_compat.
+now apply IZR_lt.
+apply bpow_gt_0.
 apply Rle_trans with (bpow (mag beta x)*bpow (1 - mag beta x)).
 apply Rmult_le_compat_r.
 apply bpow_ge_0.
@@ -1137,8 +1137,9 @@ rewrite <- mult_IZR; apply f_equal; ring.
 apply Rinv_le.
 apply Rmult_lt_0_compat.
 apply Rle_lt_0_plus_1, Rlt_le, Rlt_0_1.
-rewrite Rplus_comm, <- Rplus_assoc.
-apply Rle_lt_0_plus_1, Rlt_le,Rle_lt_0_plus_1, bpow_ge_0.
+apply Rplus_lt_0_compat.
+now apply IZR_lt.
+apply bpow_gt_0.
 apply Rmult_le_compat_l.
 apply Rlt_le,Rle_lt_0_plus_1, Rlt_le, Rlt_0_1.
 apply Rplus_le_compat_l.
diff --git a/examples/Triangle.v b/examples/Triangle.v
index 3cf50d3075c33a484c3e8e4e538c3249cb44bda4..bdcb79ac8f98a8f3dbbbac069be58d30401f1bf1 100644
--- a/examples/Triangle.v
+++ b/examples/Triangle.v
@@ -1,8 +1,5 @@
-Require Import Reals.
-Require Import Flocq.Core.Fcore.
-Require Import Flocq.Prop.Fprop_relative.
-Require Import Flocq.Prop.Fprop_Sterbenz.
-Require Import Flocq.Calc.Fcalc_ops.
+Require Import Reals Psatz.
+From Flocq Require Import Core Relative Sterbenz Operations.
 Require Import Interval.Interval_tactic.
 
 Section Delta_FLX.
@@ -12,6 +9,7 @@ Variables a b c:R.
 
 Lemma Triangle_equiv_expressions: let s:=((a+b+c)/2) in
   sqrt (s*(s-a)*(s-b)*(s-c)) = /4*sqrt ((a+(b+c))*(a+(b-c))*(c+(a-b))*(c-(a-b))).
+Proof.
 intros s.
 assert (0 <= /4).
 assert (0 < 2).
@@ -195,18 +193,7 @@ Lemma ab_exact: round_flx (a-b)=a-b.
 Proof with auto with typeclass_instances.
 apply round_generic...
 apply sterbenz_aux...
-split.
-exact bLea.
-case (Rle_or_lt a (2*b)).
-intros H; exact H.
-intros H.
-absurd (a <= b + c).
-apply Rlt_not_le.
-apply Rle_lt_trans with (2:=H).
-rewrite Rmult_plus_distr_r, Rmult_1_l.
-apply Rplus_le_compat_l.
-exact cLeb.
-exact isaTriangle1.
+lra.
 Qed.
 
 Lemma t4_exact_aux: forall (f:float beta) g,
@@ -218,7 +205,6 @@ Proof with auto with typeclass_instances.
 intros f g Hf (Hg1,Hg2) (n,Hg3).
 apply generic_format_FLX.
 exists (Float beta n (Fexp f)).
-split; simpl.
 exact Hg3.
 apply lt_IZR.
 rewrite IZR_Zpower.
@@ -252,8 +238,8 @@ Proof with auto with typeclass_instances.
 unfold t4; rewrite ab_exact.
 case cPos; intros K.
 apply round_generic...
-apply FLXN_format_generic  in Fc...
-destruct Fc as (fc, (Hfc1,Hfc2)).
+apply FLXN_format_generic in Fc...
+destruct Fc as [fc Hfc1 Hfc2].
 apply t4_exact_aux with fc.
 apply Hfc2.
 now apply Rgt_not_eq.
@@ -264,12 +250,12 @@ exact isaTriangle1.
 rewrite <-Hfc1.
 apply Rplus_le_reg_l with (-c+a); ring_simplify.
 exact bLea.
-apply FLXN_format_generic  in Fa...
-destruct Fa as (fa, (Hfa1,Hfa2)).
-apply FLXN_format_generic  in Fb...
-destruct Fb as (fb, (Hfb1,Hfb2)).
+apply FLXN_format_generic in Fa...
+destruct Fa as [fa Hfa1 Hfa2].
+apply FLXN_format_generic in Fb...
+destruct Fb as [fb Hfb1 Hfb2].
 exists (Fnum fc -(Fnum fa*Zpower beta (Fexp fa-Fexp fc) 
--Fnum fb*Zpower beta (Fexp fb-Fexp fc)))%Z. 
+-Fnum fb*Zpower beta (Fexp fb-Fexp fc)))%Z.
 rewrite Hfa1, Hfb1, Hfc1; unfold F2R; simpl.
 rewrite 2!minus_IZR.
 rewrite 2!mult_IZR.
@@ -316,12 +302,14 @@ Notation eps :=(/2*bpow (1-prec)).
 
 
 Lemma epsPos: 0 <= eps.
+Proof.
 apply Rmult_le_pos.
 auto with real.
 apply bpow_ge_0.
 Qed.
 
 Lemma err_aux: forall x y e1 e2, err x y e1 -> e1 <= e2 -> err x y e2.
+Proof.
 intros x y e1 e2 H1 H2.
 apply Rle_trans with (e1*Rabs y).
 exact H1.
@@ -332,12 +320,14 @@ Qed.
 
 
 Lemma err_0: forall x, err x x 0.
+Proof.
 intros x.
 replace (x-x) with 0%R by ring.
 rewrite Rabs_R0; right; ring.
 Qed.
 
 Lemma err_opp: forall x y e, err x y e -> err (-x) (-y) e.
+Proof.
 intros x y e H.
 replace (-x - (-y)) with (-(x-y)) by ring.
 now rewrite 2!Rabs_Ropp.
@@ -429,13 +419,10 @@ apply H.
 apply Rmult_le_reg_l with 2; auto with real.
 rewrite <- Rmult_assoc, Rinv_r.
 2:apply Rgt_not_eq, Rlt_gt; auto with real.
-rewrite 2!Rabs_right.
-rewrite Rmult_1_l, Rmult_plus_distr_r, Rmult_1_l.
-apply Rplus_le_compat_r; assumption.
-apply Rle_ge, Rplus_le_le_0_compat.
-apply Rle_trans with y2; assumption.
-assumption.
-apply Rle_ge; assumption.
+rewrite 2!Rabs_pos_eq.
+lra.
+lra.
+easy.
 Qed.
 
 
@@ -488,6 +475,7 @@ rewrite Rabs_mult; right; ring.
 Qed.
 
 Lemma err_mult_exact: forall x y e r, 0 < r -> err x y e -> err (/r*x) (/r*y) e.
+Proof.
 intros x y e r Hr H.
 assert (r <> 0).
 now apply Rgt_not_eq.
@@ -510,48 +498,32 @@ Qed.
 
 Lemma sqrt_var_maj_2: forall h : R, Rabs h <= /2 -> 
   Rabs (sqrt (1 + h) - 1) <= Rabs h / 2 + (Rabs h) * (Rabs h) / 4.
+Proof.
 intros h H1.
 case (Rle_or_lt 0 h); intros Sh.
 assert (0 <= h <= 1).
-split;[exact Sh|idtac].
-apply Rle_trans with (1:=RRle_abs _).
-apply Rle_trans with (1:=H1).
-apply Rle_trans with (/1);[idtac|right; apply Rinv_1].
-apply Interval_missing.Rle_Rinv_pos; auto with real.
-rewrite 2!Rabs_right.
+apply Rabs_le_inv in H1.
+lra.
+rewrite 2!Rabs_pos_eq.
 interval with (i_bisect_diff h).
-apply Rle_ge, Sh.
-apply Rle_ge, Rle_0_minus.
-rewrite <- sqrt_1 at 1.
-apply sqrt_le_1_alt.
-rewrite <- (Rplus_0_r 1) at 1.
-now apply Rplus_le_compat_l.
+apply Sh.
+interval.
 assert (-1/2 <= h <= 0).
-split;[idtac|left;exact Sh].
-rewrite <- (Ropp_involutive h).
-unfold Rdiv.
-rewrite Ropp_mult_distr_l_reverse, Rmult_1_l.
-apply Ropp_le_contravar.
-apply Rle_trans with (1:=RRle_abs _).
-rewrite Rabs_Ropp.
-exact H1.
+apply Rabs_le_inv in H1.
+lra.
 rewrite 2!Rabs_left.
 apply Rplus_le_reg_l with (h / 2 - h * h / 4).
 replace (h / 2 - h * h / 4 + - (sqrt (1 + h) - 1)) with ((-h/2) * (-1 + h / 2 + 2 / (sqrt(1 + h) + 1))).
-apply Rle_trans with (-h/2 * R0).
+apply Rle_trans with (-h/2 * 0%R).
 2: right ; field.
 apply Rmult_le_compat_l.
-unfold Rdiv; apply Rmult_le_pos.
-apply Ropp_0_ge_le_contravar, Rle_ge, H.
-auto with real.
+lra.
 interval with (i_bisect_diff h).
 assert (0 < (sqrt (1 + h) + 1)).
-apply Rlt_le_trans with (0+1).
-rewrite Rplus_0_l; apply Rlt_0_1.
-apply Rplus_le_compat_r, sqrt_pos.
+interval.
 replace (sqrt (1 + h) - 1) with (h / (sqrt (1 + h) + 1)).
 field.
-apply Rgt_not_eq; assumption.
+interval.
 apply Rmult_eq_reg_l with (sqrt (1 + h) + 1).
 2:apply Rgt_not_eq; assumption.
 apply trans_eq with h.
@@ -560,24 +532,13 @@ apply Rgt_not_eq; assumption.
 apply trans_eq with (Rsqr (sqrt (1 + h)) -1).
 rewrite Rsqr_sqrt.
 ring.
-apply Rle_trans with (1+(-1/2)).
-apply Rle_trans with (/2).
-auto with real.
-right; field.
-apply Rplus_le_compat_l; apply H.
+lra.
 unfold Rsqr; ring.
 exact Sh.
 apply Rlt_minus.
 rewrite <- sqrt_1 at 2.
 apply sqrt_lt_1_alt.
-split.
-apply Rle_trans with (1+-1 / 2).
-apply Rle_trans with (/2);[idtac|right; field].
-left; intuition.
-apply Rplus_le_compat_l.
-apply H.
-rewrite <- (Rplus_0_r 1) at 2.
-now apply Rplus_lt_compat_l.
+lra.
 Qed.
 
 
@@ -681,6 +642,7 @@ Qed.
 Lemma M_correct_aux: forall r, 0 <= r <= /100 ->
   2 * r ^ 8 + 15 * r ^ 7 + 50 * r ^ 6 + 97 * r ^ 5 + 120 * r ^ 4 +
    97 * r ^ 3 + 50 * r ^ 2 + 15 * r <= 52 * r ^ 2 + 15 * r.
+Proof.
 intros r (H1,H2).
 case H1; intros K.
 apply Rplus_le_reg_l with (-15*r - 51*r*r); ring_simplify.
@@ -706,6 +668,7 @@ Qed.
 (* Note: order of multiplications does not matter *)
 
 Lemma M_correct: err M E_M (15/2*eps+26*eps*eps).
+Proof.
 eapply err_aux.
 apply err_mult.
 apply err_mult.
@@ -938,9 +901,8 @@ apply generic_format_FLX.
 assert (format (round_flx (sqrt M))).
 apply generic_format_round...
 apply FLX_format_generic in H...
-destruct H as (f&Hf1&Hf2).
+destruct H as [f Hf1 Hf2].
 exists (Float beta (Fnum f) (Fexp f -2)).
-split.
 rewrite Hf1; unfold F2R; simpl.
 unfold Zminus;rewrite bpow_plus.
 replace (bpow (-(2))) with (/4).
@@ -959,7 +921,6 @@ End Delta_FLX.
 
 Section Hyp_ok.
 
-Definition radix2 := Build_radix 2 (refl_equal true).
 Definition radix10 := Build_radix 10 (refl_equal true).
 
 Lemma prec_suff_2: forall prec:Z, (7 <= prec)%Z -> (/2*bpow radix2 (1-prec) <= /100)%R.
@@ -967,18 +928,11 @@ Proof.
 intros p Hp.
 apply Rle_trans with (/2* bpow radix2 (-6))%R.
 apply Rmult_le_compat_l.
-intuition.
+lra.
 apply bpow_le.
 omega.
-simpl; rewrite <- Rinv_mult_distr.
-apply Rle_Rinv.
-apply IZR_lt; auto with zarith.
-apply IZR_lt; auto with zarith.
-apply IZR_le; auto with zarith.
-apply Rgt_not_eq, Rlt_gt.
-apply Rle_lt_0_plus_1; apply Rlt_le; exact Rlt_0_1.
-apply Rgt_not_eq, Rlt_gt.
-apply IZR_lt; auto with zarith.
+rewrite <- (Rmult_1_l (bpow _ _)).
+interval.
 Qed.
 
 
@@ -988,42 +942,34 @@ Proof.
 intros p Hp.
 apply Rle_trans with (/2* bpow radix10 (-2))%R.
 apply Rmult_le_compat_l.
-intuition.
+lra.
 apply bpow_le.
 omega.
-simpl; rewrite <- Rinv_mult_distr.
-apply Rle_Rinv.
-apply IZR_lt; auto with zarith.
-apply IZR_lt; auto with zarith.
-apply IZR_le; auto with zarith.
-apply Rgt_not_eq, Rlt_gt.
-apply Rle_lt_0_plus_1; apply Rlt_le; exact Rlt_0_1.
-apply Rgt_not_eq, Rlt_gt.
-apply IZR_lt; auto with zarith.
+rewrite bpow_exp.
+change (IZR radix10) with 10%R.
+interval.
 Qed.
 
 Lemma fourth_format_2: forall prec:Z, (0 < prec)%Z -> generic_format radix2 (FLX_exp prec) (/4).
 Proof with auto with typeclass_instances.
 intros prec Hprec.
-replace (/4)%R with (bpow radix2 (-2)).
+change (/4)%R with (bpow radix2 (-2)).
 apply generic_format_bpow'...
 unfold FLX_exp.
 omega.
-reflexivity.
 Qed.
 
 Lemma fourth_format_10: forall prec:Z, (2 <= prec)%Z -> generic_format radix10 (FLX_exp prec) (/4).
 Proof with auto with typeclass_instances.
 intros prec Hprec.
 apply generic_format_FLX.
-unfold FLX_format.
-exists (Float radix10 25 (-2)); split.
-unfold F2R; simpl.
+exists (Float radix10 25 (-2)).
+change (F2R (Float radix10 25 (-2))) with (25 / 100)%R.
 field.
 simpl.
 apply Zlt_le_trans with (10^2)%Z.
 unfold Zpower, Zpower_pos; simpl; omega.
-replace 10%Z with (radix_val radix10) by reflexivity.
+change 10%Z with (radix_val radix10).
 now apply Zpower_le.
 Qed.
 
@@ -1054,6 +1000,7 @@ Hypothesis prec_suff: (/2*bpow (1-prec) <= /100).
 Hypothesis fourth_format_gen: forall e, (emin +2 <= e)%Z -> format (/4* bpow e).
 
 Lemma fourth_format: format (/4).
+Proof.
 replace (/4) with (/4*bpow 0).
 apply fourth_format_gen.
 omega.
@@ -1155,18 +1102,7 @@ Lemma ab_exact_: round_flt (a-b)=a-b.
 Proof with auto with typeclass_instances.
 apply round_generic...
 apply sterbenz_aux...
-split.
-exact bLea.
-case (Rle_or_lt a (2*b)).
-intros H; exact H.
-intros H.
-absurd (a <= b + c).
-apply Rlt_not_le.
-apply Rle_lt_trans with (2:=H).
-rewrite Rmult_plus_distr_r, Rmult_1_l.
-apply Rplus_le_compat_l.
-exact cLeb.
-exact isaTriangle1.
+lra.
 Qed.
 
 
@@ -1180,9 +1116,7 @@ Proof with auto with typeclass_instances.
 intros f g Hf (Hg1,Hg2) (n,Hg3) Y.
 apply generic_format_FLT.
 exists (Float beta n (Fexp f)).
-split; simpl.
 exact Hg3.
-split.
 apply lt_IZR.
 rewrite IZR_Zpower.
 2: omega.
@@ -1218,8 +1152,8 @@ case cPos; intros K.
 apply round_generic...
 assert (H:(generic_format beta (FLX_exp prec) c)).
 now apply generic_format_FLX_FLT with emin.
-apply FLXN_format_generic  in H...
-destruct H as (fc, (Hfc1,Hfc2)).
+apply FLXN_format_generic in H...
+destruct H as [fc Hfc1 Hfc2].
 case (Zle_or_lt emin (Fexp fc)); intros Y.
 (* normal *)
 apply t4_exact_aux_ with fc.
@@ -1233,11 +1167,11 @@ rewrite <-Hfc1.
 apply Rplus_le_reg_l with (-c+a); ring_simplify.
 exact bLea.
 apply generic_format_FLX_FLT in Fa.
-apply FLXN_format_generic  in Fa...
-destruct Fa as (fa, (Hfa1,Hfa2)).
+apply FLXN_format_generic in Fa...
+destruct Fa as [fa Hfa1 Hfa2].
 apply generic_format_FLX_FLT in Fb.
-apply FLXN_format_generic  in Fb...
-destruct Fb as (fb, (Hfb1,Hfb2)).
+apply FLXN_format_generic in Fb...
+destruct Fb as [fb Hfb1 Hfb2].
 exists (Fnum fc -(Fnum fa*Zpower beta (Fexp fa-Fexp fc) 
 -Fnum fb*Zpower beta (Fexp fb-Fexp fc)))%Z. 
 rewrite Hfa1, Hfb1, Hfc1; unfold F2R; simpl.
@@ -1274,8 +1208,8 @@ omega.
 assumption.
 (* subnormal *)
 assert (exists f:float beta, c = F2R f /\ Fexp f = emin /\ (Z.abs (Fnum f) < beta ^ prec)%Z).
-apply FLT_format_generic  in Fc...
-destruct Fc as (ffc, (Hffc1,(Hffc2,Hffc3))).
+apply FLT_format_generic in Fc...
+destruct Fc as [ffc Hffc1 Hffc2 Hffc3].
 exists (Float beta (Fnum ffc*Zpower beta (Fexp ffc-emin)) emin).
 split.
 rewrite Hffc1; unfold F2R; simpl.
@@ -1319,10 +1253,10 @@ exact isaTriangle1.
 rewrite <-Hgc1.
 apply Rplus_le_reg_l with (-c+a); ring_simplify.
 exact bLea.
-apply FLT_format_generic  in Fa...
-destruct Fa as (fa, (Hfa1,(Hfa2,Hfa3))).
-apply FLT_format_generic  in Fb...
-destruct Fb as (fb, (Hfb1,(Hfb2,Hfb3))).
+apply FLT_format_generic in Fa...
+destruct Fa as [fa Hfa1 Hfa2 Hfa3].
+apply FLT_format_generic in Fb...
+destruct Fb as [fb Hfb1 Hfb2 Hfb3].
 rewrite Hgc2.
 exists (Fnum gc -(Fnum fa*Zpower beta (Fexp fa-emin) 
 -Fnum fb*Zpower beta (Fexp fb -emin)))%Z.
@@ -1393,7 +1327,7 @@ Proof with auto with typeclass_instances.
 intros x1 x2 Fx1 Fx2.
 case (Rle_or_lt (bpow (emin+prec-1)) (Rabs (x1+x2))); intros Y.
 (* . *)
-replace eps with  (/ 2 * Fcore_Raux.bpow beta (- prec + 1)).
+replace eps with (/ 2 * Raux.bpow beta (- prec + 1)).
 apply relative_error_N_FLT...
 apply f_equal; apply f_equal; ring.
 (* . *)
@@ -1404,12 +1338,10 @@ apply epsPos.
 apply sym_eq, round_generic...
 apply generic_format_FLT.
 apply FLT_format_generic in Fx1; apply FLT_format_generic in Fx2...
-destruct Fx1 as (f&Hf1&Hf2&Hf3).
-destruct Fx2 as (g&Hg1&Hg2&Hg3).
+destruct Fx1 as [f Hf1 Hf2 Hf3].
+destruct Fx2 as [g Hg1 Hg2 Hg3].
 exists (Fplus beta f g).
-split.
 now rewrite F2R_plus, Hf1, Hg1.
-split.
 apply lt_IZR.
 rewrite abs_IZR.
 rewrite IZR_Zpower.
@@ -1510,14 +1442,8 @@ apply Rmult_le_compat_l.
 apply H.
 apply Rmult_le_reg_l with 2; auto with real.
 rewrite <- Rmult_assoc, Rinv_r.
-2:apply Rgt_not_eq, Rlt_gt; auto with real.
-rewrite 2!Rabs_right.
-rewrite Rmult_1_l, Rmult_plus_distr_r, Rmult_1_l.
-apply Rplus_le_compat_r; assumption.
-apply Rle_ge, Rplus_le_le_0_compat.
-apply Rle_trans with y2; assumption.
-assumption.
-apply Rle_ge; assumption.
+2: now apply IZR_neq.
+rewrite 2!Rabs_pos_eq ; lra.
 Qed.
 
 Lemma err_mult_aux: forall x1 y1 e1 x2 y2 e2, format x1 -> format x2 -> err x1 y1 e1 -> err x2 y2 e2 
@@ -1541,7 +1467,7 @@ replace (round_flt (x1 * x2) - y1*y2) with ((round_flt (x1 * x2) - x1*x2)+(x1*x2
 apply Rle_trans with (1:=Rabs_triang _ _).
 apply Rle_trans with (eps*Rabs (x1*x2)+Rabs (x1 * x2 - y1 * y2)).
 apply Rplus_le_compat_r.
-replace eps with  (/ 2 * Fcore_Raux.bpow beta (- prec + 1)).
+replace eps with (/ 2 * Raux.bpow beta (- prec + 1)).
 apply relative_error_N_FLT...
 left; exact Y.
 apply f_equal; apply f_equal; ring.
@@ -1585,6 +1511,7 @@ Qed.
 Lemma err_mult_: forall x1 y1 e1 x2 y2 e2, format x1 -> format x2 -> err x1 y1 e1 -> err x2 y2 e2 
   -> (bpow (emin+prec-1) < Rabs (round_flt (x1*x2)))
   -> err (round_flt (x1*x2)) (y1*y2) (eps+(1+eps)*(e1+e2+e1*e2)).
+Proof.
 intros.
 case (err_mult_aux x1  y1 e1 x2 y2 e2); try assumption.
 easy.
@@ -1645,7 +1572,7 @@ replace (round_flt (sqrt x) - sqrt y) with ((round_flt (sqrt x) - sqrt x)+(sqrt
 apply Rle_trans with (1:=Rabs_triang _ _).
 apply Rle_trans with (eps*Rabs (sqrt x)+Rabs (sqrt x - sqrt y)).
 apply Rplus_le_compat_r.
-replace eps with  (/ 2 * Fcore_Raux.bpow beta (- prec + 1)).
+replace eps with (/ 2 * Raux.bpow beta (- prec + 1)).
 apply relative_error_N_FLT...
 rewrite Rabs_right.
 2: apply Rle_ge, sqrt_pos.
@@ -2013,10 +1940,8 @@ rewrite bpow_plus.
 apply Rmult_le_compat_r.
 apply bpow_ge_0.
 apply Rle_trans with (IZR (radix_val beta)*IZR (radix_val beta)).
-apply Rmult_le_compat;[intuition|intuition|idtac|idtac]; clear.
-apply IZR_le.
+apply (Rmult_le_compat 2 _ 2); try apply IZR_le; try easy; clear.
 apply Zle_bool_imp_le; now destruct beta.
-apply IZR_le.
 apply Zle_bool_imp_le; now destruct beta.
 right; simpl.
 unfold Zpower_pos; simpl.
@@ -2199,9 +2124,8 @@ apply generic_format_FLT.
 assert (format (round_flt (sqrt M))).
 apply generic_format_round...
 apply FLT_format_generic in H0...
-destruct H0 as (f&Hf1&Hf2&Hf3).
+destruct H0 as [f Hf1 Hf2 Hf3].
 exists (Float beta (Fnum f) (Fexp f -2)).
-split.
 rewrite Hf1; unfold F2R; simpl.
 unfold Zminus;rewrite bpow_plus.
 replace (bpow (-(2))) with (/4).
@@ -2209,7 +2133,6 @@ ring.
 simpl; unfold Zpower_pos;simpl.
 rewrite Hradix; apply f_equal.
 simpl; ring.
-split.
 now simpl.
 simpl.
 assert (emin+1+prec < prec+Fexp f)%Z;[idtac|omega].
@@ -2273,16 +2196,15 @@ Lemma fourth_format_gen_10: forall prec emin e:Z, (2 <= prec)%Z -> (emin +2 <= e
 Proof with auto with typeclass_instances.
 intros prec emin e Hprec H.
 apply generic_format_FLT.
-unfold FLT_format.
-exists (Float radix10 25 (e-2)); split.
+exists (Float radix10 25 (e-2)).
 unfold F2R; simpl.
 unfold Zminus; rewrite bpow_plus.
-simpl; field.
-split.
+change (bpow radix10 (-(2))) with (/100)%R.
+field.
 simpl.
 apply Zlt_le_trans with (10^2)%Z.
 unfold Zpower, Zpower_pos; simpl; omega.
-replace 10%Z with (radix_val radix10) by reflexivity.
+change 10%Z with (radix_val radix10).
 now apply Zpower_le.
 simpl.
 omega.