diff --git a/src_common/ieee/coq/Finterval.v b/src_common/ieee/coq/Finterval.v
index a6d3e738034c215daadf4121ece8f89cc7491443..00e5abc2c090eff408e04cbb24b6b81487a18d70 100644
--- a/src_common/ieee/coq/Finterval.v
+++ b/src_common/ieee/coq/Finterval.v
@@ -119,8 +119,6 @@ Axiom add_le_compat :
     x2 <= y2 ->
     Bplus m x1 x2 <= Bplus m y1 y2.
 
-Check (Bplus_correct).
-
 Lemma Iadd2_check :
   forall m I₁ I₂, check I₁ -> check I₂ -> check (Iadd2 m I₁ I₂).
 Proof.
diff --git a/src_common/ieee/coq/Futils.v b/src_common/ieee/coq/Futils.v
index 051f2e9ce07a8eace02c3d6f933fda825e58316e..66bcff24ee414ad5220d0dc720f56cab4eddf055 100644
--- a/src_common/ieee/coq/Futils.v
+++ b/src_common/ieee/coq/Futils.v
@@ -98,7 +98,7 @@ Definition dont_overflow (m : mode) (op : R -> R -> R) (x y : float) : bool :=
   let rsum := Generic_fmt.round Zaux.radix2 fexp (round_mode m) (op (B2R x) (B2R y)) in
   Raux.Rlt_bool (Rabs rsum) fmax.
 
-Lemma Bplus_not_nan :
+Lemma Bplus_not_nan_inv :
   forall m (x y : float),
   is_nan (Bplus m x y) = false ->
   is_nan x = false /\ is_nan y = false.
@@ -143,12 +143,11 @@ Qed.
 
 Lemma Bplus_correct_full :
   forall (m : mode) (x y : float),
-  is_nan x = false ->
-  is_nan y = false ->
   is_nan (Bplus m x y) = false ->
   B2Rx (Bplus m x y) = round m (add (B2Rx x) (B2Rx y)).
 Proof.
-  intros m x y HnanX HnanY HnanS.
+  intros m x y HnanS.
+  destruct (Bplus_not_nan_inv _ _ _ HnanS) as [HnanX HnanY].
   induction x as [ [ ] | [ ] | | ] eqn:Ex, y as [ [ ] | [ ] | | ] eqn:Ey; try easy.
   - simpl (Bplus m (B754_zero _) _).
     simpl (B2Rx (B754_zero _)).
@@ -158,7 +157,8 @@ Proof.
     rewrite add_0_l. destruct m; auto using round_0.
   - simpl (Bplus m (B754_zero true) _).
     simpl (B2Rx (B754_zero _)).
-    rewrite add_0_l. admit.
+    rewrite add_0_l.
+    apply round_id.
   - simpl (Bplus m (B754_zero _) _).
     simpl (B2Rx (B754_zero _)).
     rewrite add_0_r. destruct m; auto using round_0.
@@ -168,18 +168,16 @@ Proof.
     apply round_0.
   - simpl (Bplus m (B754_zero _) _).
     rewrite add_0_l.
-    admit.
+    apply round_id.
   - simpl (Bplus m _ (B754_zero _)).
     rewrite add_0_r.
-    admit.
+    apply round_id.
   - simpl (Bplus m _ (B754_zero _)).
     rewrite add_0_r.
-    admit.
+    apply round_id.
   - admit.
 Admitted.
 
-Check (binary_overflow).
-
 End Utils.
 
 Arguments le_not_nan {prec} {emax}.
diff --git a/src_common/ieee/coq/Rextended.v b/src_common/ieee/coq/Rextended.v
index 48d2958a18b32c4668165380fed049c4556be96f..67887e36f1213fb9a05a5f9fa27b03bdd8252009 100644
--- a/src_common/ieee/coq/Rextended.v
+++ b/src_common/ieee/coq/Rextended.v
@@ -7,6 +7,38 @@ From Coq Require Import ZArith Psatz Reals.
 
 Set Implicit Arguments.
 
+Section Rutils.
+
+Definition sign (r : R) :=
+  Raux.Rlt_bool r 0.
+
+Lemma sign_pos_inv :
+  forall r, sign r = false -> (0 <= r)%R.
+Proof.
+  intros.
+  unfold sign in H.
+  now destruct (Raux.Rlt_bool_spec r 0).
+Qed.
+
+Lemma sign_neg_inv :
+  forall r, sign r = true -> (r <= 0)%R.
+Proof.
+  intros.
+  unfold sign in H. left.
+  now destruct (Raux.Rlt_bool_spec r 0).
+Qed.
+
+Lemma sign_neg_inv_strict:
+  forall r, sign r = true -> (r < 0)%R.
+Proof.
+  intros.
+  unfold sign in H.
+  now destruct (Raux.Rlt_bool_spec r 0).
+Qed.
+
+End Rutils.
+
+
 Section Rextended.
 
 Variable prec : Z.
@@ -14,10 +46,6 @@ Variable emax : Z.
 Context (Hprec : FLX.Prec_gt_0 prec).
 Context (Hemax : Prec_lt_emax prec emax).
 
-Check (Bplus_correct).
-
-Check (B754_finite).
-
 Definition float := binary_float prec emax.
 
 (** Reals extended with +oo, -oo *)
@@ -29,8 +57,6 @@ Definition R_imax : R := Raux.bpow Zaux.radix2 emax.
 
 Definition R_fmax : R := Raux.bpow Zaux.radix2 emax - Raux.bpow Zaux.radix2 (emax - prec).
 
-Definition F_imax : float := B754_infinity false.
-
 Program Definition F_fmax : float := B754_finite false (Z.to_pos (Zpower 2 prec - 1)%Z) (emax - prec) _.
 Next Obligation.
   refine (binary_overflow_correct prec emax _ _ mode_ZR false).
@@ -58,6 +84,7 @@ Proof.
     + lia.
 Qed.
 
+(** Futils *)
 Lemma le_Bleb :
   forall (x y : float),
     is_finite x = true ->
@@ -73,28 +100,6 @@ Proof.
   apply Raux.Rcompare_Gt_inv in E; lra.
 Qed.
 
-Lemma testeq:
-  (Raux.bpow Zaux.radix2 emax - Raux.bpow Zaux.radix2 (emax - prec) = 
-  IZR (Z.pos (Z.to_pos (2 ^ prec - 1))) * Raux.bpow Zaux.radix2 (emax - prec))%R.
-Proof.
-  unfold FLX.Prec_gt_0 in Hprec.
-  unfold Prec_lt_emax in Hemax.
-  assert (0 < emax)%Z by lia.
-  destruct prec eqn:E; try easy.
-  rewrite Z2Pos.id.
-  - rewrite <- E, minus_IZR.
-    replace 2%Z with (Zaux.radix_val Zaux.radix2) by auto.
-    rewrite Raux.IZR_Zpower by lia.
-    rewrite Rmult_minus_distr_r.
-    rewrite <- Raux.bpow_plus.
-    replace (prec + (emax - prec))%Z with emax by lia.
-    lra.
-  - assert (1 < 2 ^ (Z.pos p))%Z.
-    + replace 2%Z with (Zaux.radix_val Zaux.radix2) by auto.
-      apply Zaux.Zpower_gt_1; lia.
-    + lia.
-Qed.
-
 Lemma F_fmax_max :
   forall (x : float), is_finite x = true -> Bleb x F_fmax = true. 
 Proof.
@@ -118,15 +123,11 @@ Lemma F_fmax_min :
 Proof.
   intros [ [ ] | [ ] | | [ ] m e Hbound'] Fx; auto.
   apply le_Bleb; auto.
-  rewrite Bopp_finite, B2R_Bopp, B2R_Bopp, <- R2F_fmax.
+  rewrite pos_Bopp_neg, B2R_Bopp, B2R_Bopp, <- R2F_fmax.
   apply Ropp_le_contravar.
   now apply bounded_le_emax_minus_prec.
 Qed.
 
-Lemma Bopp_eq :
-  forall m e Hb, @B754_finite prec emax true m e Hb = Bopp (B754_finite false m e Hb).
-Proof. reflexivity. Qed.
-
 Lemma Bleb_le :
   forall x y : float, is_finite x = true -> is_finite y = true ->
     Bleb x y = true -> (B2R x <= B2R y)%R.
@@ -140,21 +141,6 @@ Proof.
   + apply Raux.Rcompare_Lt_inv in E; lra.
 Qed.
 
-Lemma sfmax_min:
-  forall (x : float), is_finite x = true -> Bleb (sfmax true) x = true. 
-Proof.
-  intros; simpl.
-  set (Hbound := sfmax_obligation_1 true).
-  destruct x as [ [ ] | [ ] | | [ ] m e Hbound'] eqn:Ex; try easy.
-  apply le_Bleb; try easy.
-  unfold sfmax.
-  rewrite Bopp_eq, Bopp_eq.
-  rewrite B2R_Bopp, B2R_Bopp.
-  apply Ropp_le_contravar.
-  apply Bleb_le; try easy.
-  now apply sfmax_max.
-Qed.
-
 Definition leb (x y : Rx) :=
   match x with
   | Inf true => true
@@ -175,12 +161,12 @@ Definition fexp := SpecFloat.fexp prec emax.
 Definition do_overflow (m : mode) (x : R) : bool :=
   let fexp := SpecFloat.fexp prec emax in
   let rsum := Generic_fmt.round Zaux.radix2 fexp (round_mode m) x in
-  Raux.Rle_bool fmax (Rabs rsum).
+  Raux.Rle_bool R_imax (Rabs rsum).
 
 Definition dont_overflow (m : mode) (x : R) : bool :=
   let fexp := SpecFloat.fexp prec emax in
   let rsum := Generic_fmt.round Zaux.radix2 fexp (round_mode m) x in
-  Raux.Rlt_bool (Rabs rsum) fmax.
+  Raux.Rlt_bool (Rabs rsum) R_imax.
 
 Lemma do_overflow_false :
   forall m r, do_overflow m r = false -> dont_overflow m r = true.
@@ -189,15 +175,28 @@ Proof.
   now rewrite <- Raux.negb_Rlt_bool, H.
 Qed.
 
-Definition sign (r : R) :=
-  Raux.Rlt_bool r 0.
+Lemma F2R_congr :
+  forall m1 e1 m2 e2, m1 = m2 -> e1 = e2 ->
+  @Defs.F2R Zaux.radix2 {| Defs.Fnum := m1; Defs.Fexp := e1 |} = 
+  @Defs.F2R Zaux.radix2 {| Defs.Fnum := m2; Defs.Fexp := e2 |}.
+Proof. congruence. Qed.
+
+Lemma dont_overflow_inv :
+  forall m (r : R),
+    do_overflow m r = false ->
+    exists (f : float), Generic_fmt.round Zaux.radix2 (SpecFloat.fexp prec emax) (round_mode m) r = B2R f /\ is_finite f = true.
+    (* exists mr er Hb, Generic_fmt.round Zaux.radix2 fexp (round_mode m) r = @B2R prec emax (B754_finite (sign r) mr er Hb). *)
+Proof.
+Admitted.
+
+
 
 Definition round (m : mode) (r : Rx) : Rx :=
   match r with
   | Real x =>
     if do_overflow m x then
       if overflow_to_inf m (sign x) then Inf (sign x)
-      else Real (B2R (sfmax (sign x)))
+      else Real (B2R (if sign x then Bopp F_fmax else F_fmax))
     else
       Real (Generic_fmt.round Zaux.radix2 (SpecFloat.fexp prec emax) (round_mode m) x)
   | _  => r
@@ -222,11 +221,11 @@ Proof.
   now destruct (Raux.Rle_bool_spec r1 r2).
 Qed.
 
-Lemma fmax_gt_0: (fmax > 0)%R.
+Lemma R_imax_gt_0: (R_imax > 0)%R.
   apply Raux.bpow_gt_0.
 Qed.
 
-Lemma sfmax_gt_0: (B2R (sfmax false) >= 0)%R.
+Lemma F_fmax_ge_0: (B2R F_fmax >= 0)%R.
   simpl.
   unfold Defs.F2R; simpl.
   apply Rle_ge, Rmult_le_pos.
@@ -237,11 +236,11 @@ Qed.
 Ltac fformat :=
   try intuition; try apply fexp_correct.
 
-Theorem generic_format_fmax :
-  Generic_fmt.generic_format Zaux.radix2 fexp fmax.
+Theorem generic_format_Rimax :
+  Generic_fmt.generic_format Zaux.radix2 fexp R_imax.
 Proof.
   intros.
-  red; unfold Defs.F2R, fmax; simpl.
+  red; unfold Defs.F2R, R_imax; simpl.
   rewrite <- Generic_fmt.scaled_mantissa_generic.
   + unfold Generic_fmt.scaled_mantissa.
     rewrite Rmult_assoc, Rmult_comm.
@@ -255,12 +254,12 @@ Proof.
     lia.
 Qed.
 
-Theorem round_fmax :
-  forall m, Generic_fmt.round Zaux.radix2 fexp (round_mode m) fmax = fmax.
+Theorem round_Rimax :
+  forall m, Generic_fmt.round Zaux.radix2 fexp (round_mode m) R_imax = R_imax.
 Proof.
   intros.
   apply Generic_fmt.round_generic; intuition.
-  apply generic_format_fmax.
+  apply generic_format_Rimax.
 Qed.
 
 Lemma Rlt_lt :
@@ -272,20 +271,20 @@ Proof.
   now inversion Hp.
 Qed.
 
-Lemma fmax_float :
-  exists m e, fmax = Defs.F2R (Defs.Float Zaux.radix2 m e).
+Lemma Rimax_float :
+  exists m e, R_imax = Defs.F2R (Defs.Float Zaux.radix2 m e).
 Proof.
   exists 1%Z.
-  unfold fmax, Defs.F2R; simpl.
+  unfold R_imax, Defs.F2R; simpl.
   eexists.
   symmetry.
   apply Rmult_1_l.
 Qed.
 
-Lemma incr_sfmax_fmax :
-  @Defs.F2R Zaux.radix2 {| Defs.Fnum := (Zpower 2 prec - 1 + 1)%Z ; Defs.Fexp := (emax - prec) |} = fmax.
+Lemma incr_R_fmax_R_imax :
+  @Defs.F2R Zaux.radix2 {| Defs.Fnum := (Zpower 2 prec - 1 + 1)%Z ; Defs.Fexp := (emax - prec) |} = R_imax.
 Proof.
-  unfold Defs.F2R, fmax; simpl.
+  unfold Defs.F2R, R_imax; simpl.
   replace (2 ^ prec - 1 + 1)%Z with (2 ^ prec)%Z by lia.
   rewrite (Raux.IZR_Zpower Zaux.radix2).
   + rewrite <- Raux.bpow_plus.
@@ -296,39 +295,11 @@ Proof.
     lia.
 Qed.
 
-Theorem dont_overflow_round_sfmax :
-  forall m r,
-    dont_overflow m r = true ->
-    (Generic_fmt.round Zaux.radix2 fexp (round_mode m) r <= B2R (sfmax false))%R.
-Proof.
-  intros.
-  (* unfold Generic_fmt.round; simpl.
-  unfold Defs.F2R; simpl. *)
-  unfold dont_overflow in H.
-  apply Rlt_lt in H.
-  eapply Rle_trans. apply Rle_abs.
-  apply Rnot_gt_le; intros Hcontr.
-  apply Rgt_lt in Hcontr.
-  set (r' := Rabs (Generic_fmt.round Zaux.radix2 (SpecFloat.fexp prec emax) (round_mode m) r)).
-  pose proof (Rabs_pos r').
-  destruct H0 as [Hr' | Hr'].
-  + 
-    pose proof (Generic_fmt.generic_format_round_pos Zaux.radix2 fexp (round_mode m) _ Hr').
-    assert (~(Generic_fmt.generic_format Zaux.radix2 fexp r')); admit.
-  + symmetry in Hr'. apply Raux.Rabs_eq_R0 in Hr'.
-    subst r'.
-    rewrite Hr' in H.
-    unfold fexp in Hcontr.
-    rewrite Hr' in Hcontr.
-    pose proof (sfmax_gt_0).
-    lra.
-Admitted.
-
 Theorem do_overflow_iff:
   forall m x,
     let fexp := SpecFloat.fexp prec emax in
     let rx := Generic_fmt.round Zaux.radix2 fexp (round_mode m) x in
-    do_overflow m x = true <-> (Raux.Rle_bool fmax rx = true \/ Raux.Rle_bool rx (-fmax)%R = true).
+    do_overflow m x = true <-> (Raux.Rle_bool R_imax rx = true \/ Raux.Rle_bool rx (-R_imax)%R = true).
 Proof.
   intros; split; intros.
   - unfold do_overflow in H.
@@ -345,8 +316,8 @@ Proof.
   - destruct H; apply Raux.Rle_bool_true; apply Rle_le in H.
     + eauto using Rle_trans, H, Rle_abs.
     + apply Ropp_le_contravar in H.
-      replace (--fmax)%R with fmax in H by lra.
-      pose proof fmax_gt_0.
+      replace (--R_imax)%R with R_imax in H by lra.
+      pose proof R_imax_gt_0.
       assert (0 <= -rx)%R by lra.
       assert (0 > rx)%R by lra.
       assert (-rx > rx)%R by lra.
@@ -356,51 +327,9 @@ Proof.
 Qed.
 
 
-Lemma sign_false_0 :
-  forall r, sign r = false -> (0 <= r)%R.
-Proof.
-  intros.
-  unfold sign in H.
-  now destruct (Raux.Rlt_bool_spec r 0).
-Qed.
 
-Lemma sign_true_0 :
-  forall r, sign r = true -> (r <= 0)%R.
-Proof.
-  intros.
-  unfold sign in H. left.
-  now destruct (Raux.Rlt_bool_spec r 0).
-Qed.
 
-Lemma sign_true_0_strict:
-  forall r, sign r = true -> (r < 0)%R.
-Proof.
-  intros.
-  unfold sign in H.
-  now destruct (Raux.Rlt_bool_spec r 0).
-Qed.
 
-Lemma dont_overflow_iff :
-  forall m (r : R),
-    do_overflow m r = false ->
-    exists s mr er Hb, Generic_fmt.round Zaux.radix2 fexp (round_mode m) r = @B2R prec emax (B754_finite s mr er Hb) /\ sign r = s.
-Proof.
-  intros m r Hr.
-  exists (sign r).
-  exists (Z.to_pos (Raux.Ztrunc (Generic_fmt.scaled_mantissa Zaux.radix2 fexp r))).
-  exists (Generic_fmt.cexp Zaux.radix2 fexp r).
-  eexists; split; auto.
-  simpl.
-  (* intros m r Hr; repeat eexists.
-  apply do_overflow_false in Hr.
-  unfold dont_overflow in Hr.
-  pose proof (H1 := Raux.Rlt_bool_spec (Rabs (Generic_fmt.round Zaux.radix2 (SpecFloat.fexp prec emax) (round_mode m) r)) fmax).
-  rewrite Hr in H1.
-  inversion H1 as [H|].
-  clear H1; clear Hr.
-  destruct (sign r) eqn:Hs.
-  + apply sign_true_0_strict in Hs. *)
-Admitted.
 
 Lemma overflow_le :
   forall m r1 r2, 
@@ -419,8 +348,8 @@ Proof.
     + now apply fexp_correct.
     + intuition.
   - apply Rle_le in H.
-    assert (-fmax < 0)%R.
-    { assert (fmax > 0)%R by apply fmax_gt_0. lra. }
+    assert (-R_imax < 0)%R.
+    { assert (R_imax > 0)%R by apply R_imax_gt_0. lra. }
     pose proof H0.
     apply Rlt_le in H1.
     eapply Generic_fmt.round_le in Hr1.
@@ -447,15 +376,15 @@ Proof.
   intros m r1 r2 Hle Hr1 Ho.
   rewrite do_overflow_iff in Ho. destruct Ho as [H | H].
   - apply Rle_le in H.
-    rewrite <- (round_fmax m) in H.
+    rewrite <- (round_Rimax m) in H.
     eapply (Generic_fmt.round_le Zaux.radix2 fexp (round_mode m)) in Hr1; intuition.
     rewrite Generic_fmt.round_0 in Hr1.
-    assert (Generic_fmt.round Zaux.radix2 fexp (round_mode m) fmax <= 0)%R.
+    assert (Generic_fmt.round Zaux.radix2 fexp (round_mode m) R_imax <= 0)%R.
     + eapply Rle_trans.
       * apply H.
       * apply Hr1.
-    + pose proof fmax_gt_0.
-      rewrite (round_fmax m) in H0.
+    + pose proof R_imax_gt_0.
+      rewrite (round_Rimax m) in H0.
       lra.
     + intuition.
   - apply Rle_le in H.
@@ -474,7 +403,7 @@ Proof.
   intros m.
   unfold round.
   assert (H: do_overflow m 0 = false).
-  { unfold do_overflow, fmax.
+  { unfold do_overflow, R_imax.
     rewrite Generic_fmt.round_0 by fformat.
     rewrite Rabs_R0.
     apply Raux.Rle_bool_false.
@@ -487,135 +416,84 @@ Qed.
 Theorem round_le:
   forall (m : mode) (r1 r2 : Rx), leb r1 r2 = true -> leb (round m r1) (round m r2) = true.
 Proof.
-  intros m [ r1 | [] ] [r2 | []] H.
+  intros m [ r1 | [] ] [r2 | []] H; try easy.
+  Ltac fbounded :=
+    match goal with
+    | [ Ho1 : do_overflow _ _ = false |- _ ] =>
+      apply Raux.Rle_bool_true;
+      destruct (dont_overflow_inv _ _ Ho1) as (f & [?Hreq ?Hf]);
+      rewrite ?Hreq; first [now apply Bleb_le, F_fmax_min | now apply Bleb_le, F_fmax_max ]
+  end.
+  Ltac freals :=
+    match goal with
+    | [ H : Raux.Rle_bool _ _ = true |- _ ] =>
+      apply Raux.Rle_bool_true; apply Rle_le in H;
+      now apply Generic_fmt.round_le; fformat
+  end.
+  Ltac finfinites :=
+    simpl; now destruct overflow_to_inf eqn:?, do_overflow eqn:?, sign eqn:?.
+  Ltac absurd_sign :=
+    match goal with
+    | [ Hs2 : sign _ = true, Hs1 : sign _ = false, H : Raux.Rle_bool _ _ = true |- _ ] =>
+      now rewrite (sign_le _ _ Hs1 Hs2) in H
+  end.
+  Ltac absurd_mode :=
+    match goal with
+    | [ m : mode |- _] => now destruct m
+  end.
+  Ltac absurd_overflow :=
+    match goal with
+    | [ H : Raux.Rle_bool _ _ = true,
+        Hs : sign _ = false,
+        Ho1 : do_overflow _ _ = true,
+        Ho2 : do_overflow _ _ = false
+        |- _ 
+      ] => apply Rle_le in H; now rewrite (overflow_le _ H (sign_pos_inv _ Hs) Ho1) in Ho2
+    | [ H : Raux.Rle_bool _ _ = true,
+        Hs : sign _ = true,
+        Ho1 : do_overflow _ _ = false,
+        Ho2 : do_overflow _ _ = true
+      |- _
+      ] => apply Rle_le in H; now rewrite (overflow_le' _ H (sign_neg_inv _ Hs) Ho2) in Ho1
+    | [ H : Raux.Rle_bool _ _ = false,
+      Hs : sign _ = true,
+      Ho1 : do_overflow _ _ = true,
+      Ho2 : do_overflow _ _ = false
+      |- _ 
+    ] => apply Rle_le in H; now rewrite (overflow_le' _ H (sign_neg_inv _ Hs) Ho2) in Ho1
+    | [ H1 : overflow_to_inf _ _ = true, H2 : overflow_to_inf _ _ = false |- _ ] =>
+      now rewrite H1 in H2
+    end.
+  Ltac absurd_case :=
+    match goal with
+    | [r1 : R, r2 : R |- _ ] =>
+      try absurd_mode; try absurd_sign; absurd_overflow
+  end.
+  Ltac sign_analysis :=
+    match goal with
+    | [r1 : R, r2 : R |- _ ] =>
+      destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; auto
+  end.
   - simpl in H. unfold round.
     destruct (do_overflow m r1) eqn:Ho1;
-    destruct (overflow_to_inf m (sign r1)) eqn:Hi1;
     destruct (do_overflow m r2) eqn:Ho2;
-    destruct (overflow_to_inf m (sign r2)) eqn:Hi2.
-    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; auto.
-      now rewrite (sign_le _ _ Hs1 Hs2) in H.
-    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; simpl; auto.
-      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
-      * now destruct m.
-    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; simpl; auto.
-      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
-      * apply Rle_le in H.
-        now rewrite (overflow_le m H (sign_false_0 r1 Hs1) Ho1) in Ho2.
-    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; simpl; auto.
-      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
-      * apply Rle_le in H.
-        now rewrite (overflow_le m H (sign_false_0 r1 Hs1) Ho1) in Ho2.
-    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; simpl; auto.
-      * now destruct m.
-      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
-    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; simpl; auto.
-      * unfold Raux.Rle_bool.
-        destruct Raux.Rcompare eqn:E; try easy.
-        apply Raux.Rcompare_Gt_inv in E; lra.
-      * unfold Raux.Rle_bool.
-        destruct Raux.Rcompare eqn:E; try easy.
-        apply Raux.Rcompare_Gt_inv in E.
-        unfold Defs.F2R in E; simpl in E.
-        apply Rmult_lt_reg_r in E.
-        ** apply lt_IZR in E; lia.
-        ** apply Raux.bpow_gt_0.
-      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
-      * unfold Raux.Rle_bool.
-        destruct Raux.Rcompare eqn:E; try easy.
-        apply Raux.Rcompare_Gt_inv in E; lra.
-    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2.
-      * now rewrite Hi2 in Hi1.
-      * apply Raux.Rle_bool_true.
-        destruct (dont_overflow_iff _ _ Ho2) as (s & mr & er & ? & [Hreq Hrs]).
-        unfold fexp in Hreq; rewrite Hreq.
-        rewrite <- Hrs, Hs2.
-        now apply Bleb_le.
-      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
-      * apply Rle_le in H.
-        now rewrite (overflow_le m H (sign_false_0 r1 Hs1) Ho1) in Ho2.
-    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2.
-      * unfold leb.
-        apply Raux.Rle_bool_true.
-        destruct (dont_overflow_iff _ _ Ho2) as (s & mr & er & ? & [Hreq Hrs]).
-        unfold fexp in Hreq; rewrite Hreq.
-        rewrite <- Hrs, Hs2.
-        apply Bleb_le; try easy.
-        now apply sfmax_min.
-      * unfold leb. apply Raux.Rle_bool_true.
-        destruct (dont_overflow_iff _ _ Ho2) as (s & mr & er & ? & [Hreq Hrs]).
-        unfold fexp in Hreq; rewrite Hreq.
-        rewrite <- Hrs, Hs2.
-        now apply Bleb_le.
-      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
-      * apply Rle_le in H.
-        now rewrite (overflow_le m H (sign_false_0 r1 Hs1) Ho1) in Ho2.
-    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; simpl; auto.
-      * apply Rle_le in H.
-        now rewrite (overflow_le' m H (sign_true_0 r2 Hs2) Ho2) in Ho1.
-      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
-    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2.
-      * apply Rle_le in H.
-        now rewrite (overflow_le' m H (sign_true_0 r2 Hs2) Ho2) in Ho1.
-      * apply Raux.Rle_bool_true.
-        destruct (dont_overflow_iff _ _ Ho1) as (s & mr & er & ? & [Hreq Hrs]).
-        unfold fexp in Hreq; rewrite Hreq.
-        rewrite <- Hrs, Hs1.
-        now apply Bleb_le.
-      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
-      * apply Raux.Rle_bool_true.
-        destruct (dont_overflow_iff _ _ Ho1) as (s & mr & er & ? & [Hreq Hrs]).
-        unfold fexp in Hreq; rewrite Hreq.
-        rewrite <- Hrs, Hs1.
-        apply Bleb_le; try easy.
-        now apply sfmax_max.
-    + simpl. apply Raux.Rle_bool_true.
-      apply Rle_le in H.
-      apply Generic_fmt.round_le; fformat; auto.
-    + simpl. apply Raux.Rle_bool_true.
-      apply Rle_le in H.
-      apply Generic_fmt.round_le; fformat; auto.
-    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; try easy.
-      * now destruct m.
-      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
-    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; try easy.
-      * apply Rle_le in H.
-        now rewrite (overflow_le' m H (sign_true_0 r2 Hs2) Ho2) in Ho1.
-      * apply Raux.Rle_bool_true.
-        destruct (dont_overflow_iff _ _ Ho1) as (s & mr & er & ? & [Hreq Hrs]).
-        unfold fexp in Hreq; rewrite Hreq.
-        rewrite <- Hrs, Hs1.
-        now apply Bleb_le.
-      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
-      * apply Raux.Rle_bool_true.
-        destruct (dont_overflow_iff _ _ Ho1) as (s & mr & er & ? & [Hreq Hrs]).
-        unfold fexp in Hreq; rewrite Hreq.
-        rewrite <- Hrs, Hs1.
-        apply Bleb_le; try easy.
-        now apply sfmax_max.
-    + simpl. apply Raux.Rle_bool_true.
-      apply Generic_fmt.round_le; fformat; auto.
-      now apply Rle_le in H.
-    + simpl. apply Raux.Rle_bool_true.
-      apply Generic_fmt.round_le; fformat; auto.
-      now apply Rle_le in H.
-  - discriminate.
-  - simpl.
-    destruct (overflow_to_inf) eqn:Hi;
-    destruct (do_overflow) eqn:Ho;
-    destruct (sign) eqn:Hs;
-    try easy.
-  - simpl.
-    reflexivity.
-  - simpl. reflexivity.
-  - simpl. reflexivity.
-  - simpl.
-    destruct (overflow_to_inf) eqn:Hi;
-    destruct (do_overflow) eqn:Ho;
-    destruct (sign) eqn:Hs;
-    try easy.
-  - discriminate.
-  - simpl. reflexivity.
+    destruct (overflow_to_inf m (sign r1)) eqn:Hi1;
+    destruct (overflow_to_inf m (sign r2)) eqn:Hi2;
+    (try freals); sign_analysis; try absurd_case; try fbounded; simpl.
+    + unfold Raux.Rle_bool.
+      destruct Raux.Rcompare eqn:E; try easy.
+      apply Raux.Rcompare_Gt_inv in E; lra.
+    + unfold Raux.Rle_bool.
+      destruct Raux.Rcompare eqn:E; try easy.
+      apply Raux.Rcompare_Gt_inv in E.
+      unfold Defs.F2R in E; simpl in E.
+      apply Rmult_lt_reg_r in E.
+      * apply lt_IZR in E; lia.
+      * apply Raux.bpow_gt_0.
+    + unfold Raux.Rle_bool.
+      destruct Raux.Rcompare eqn:E; try easy.
+      apply Raux.Rcompare_Gt_inv in E; lra.
+  - finfinites.
 Qed.
 
 Lemma round_inf :
@@ -681,6 +559,12 @@ Lemma B2Rx_finite :
   is_finite f = true -> B2Rx f = Real (B2R f).
 Proof. now destruct f. Qed.
 
+Lemma round_id :
+  forall m (f : float),
+    B2Rx f = round m (B2Rx f).
+Proof.
+Admitted.
+
 Lemma B2Rx_le :
   forall (x y : float),
   is_nan x = false ->