diff --git a/src_common/ieee/coq/.nra.cache b/src_common/ieee/coq/.nra.cache
index d5f5a6b53198bfebac45c7c193bb90e4c8f0c71b..1e48d00680c8db820e245fdf2ea46806e94456c1 100644
Binary files a/src_common/ieee/coq/.nra.cache and b/src_common/ieee/coq/.nra.cache differ
diff --git a/src_common/ieee/coq/Correction_thms.v b/src_common/ieee/coq/Correction_thms.v
index 9497ce7cf3901e7aa67d321fe3635a321dc74543..2f67e802709a915931b34598981858df1a7a908e 100644
--- a/src_common/ieee/coq/Correction_thms.v
+++ b/src_common/ieee/coq/Correction_thms.v
@@ -11,6 +11,17 @@ Context (Hemax : Prec_lt_emax prec emax).
 
 Definition float : Type := binary_float prec emax.
 
+
+Lemma B2SF_eq :
+  forall (x : float) y H, B2SF x = y -> x = SF2B y H.
+Proof.
+  intros.
+  apply B2SF_inj.
+  rewrite H0.
+  symmetry.
+  apply B2SF_SF2B.
+Qed.
+
 Lemma Bplus_correct :
   forall (m : mode) (x y : float),
   is_nan (Bplus m x y) = false ->
@@ -24,6 +35,200 @@ Proof.
   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; try compute0.
-Admitted.
+  unfold add.
+  repeat rewrite (B2Rx_finite (B754_finite _ _ _ _)); auto.
+  unfold round.
+  assert (Fx : is_finite x = true) by (rewrite Ex; auto).
+  assert (Fy : is_finite y = true) by (rewrite Ey; auto).
+  pose proof (Bplus_correct _ _ _ _ m x y Fx Fy).
+  destruct (do_overflow _ _ _ _) eqn:Ho1.
+  - apply do_overflow_true in Ho1.
+    unfold dont_overflow in Ho1.
+    rewrite <- Ex, <- Ey in *.
+    unfold R_imax in Ho1.
+    rewrite Ho1 in H.
+    destruct H as [H1 H2].
+    apply (B2SF_eq _ _ (binary_overflow_correct _ _ _ _ _ _)) in H1.
+    destruct m eqn:Em, (sign (B2R x + B2R y)) eqn:Hs.
+    + simpl in *. rewrite H1; simpl. 
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_neg_inv in Hs.
+      assert (forall x, IZR (Z.pos x) > 0)%R.
+      { induction x; try lra.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+      }
+      pose proof (H m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_pos_inv in Hs.
+      assert (forall x, IZR (Z.neg x) < 0)%R.
+      { induction x; try lra.
+        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
+          apply IZR_lt; lia.
+        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
+          apply IZR_lt; lia.
+      }
+      pose proof (H m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_neg_inv in Hs.
+      assert (forall x, IZR (Z.pos x) > 0)%R.
+      { induction x; try lra.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+      }
+      pose proof (H m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_pos_inv in Hs.
+      change (Z.neg m2) with (- Z.pos m2)%Z in Hs.
+      change (Z.neg m3) with (- Z.pos m3)%Z in Hs.
+      repeat rewrite opp_IZR in Hs.
+      assert (forall x, IZR (Z.pos x) > 0)%R.
+      { induction x; try lra.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+      }
+      pose proof (H m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_neg_inv in Hs.
+      assert (forall x, IZR (Z.pos x) > 0)%R.
+      { induction x; try lra.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+      }
+      pose proof (H m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_pos_inv in Hs.
+      assert (forall x, IZR (Z.neg x) < 0)%R.
+      { induction x; try lra.
+        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
+          apply IZR_lt; lia.
+        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
+          apply IZR_lt; lia.
+      }
+      pose proof (H m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_neg_inv in Hs.
+      assert (forall x, IZR (Z.pos x) > 0)%R.
+      { induction x; try lra.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+      }
+      pose proof (H m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_pos_inv in Hs.
+      assert (forall x, IZR (Z.neg x) < 0)%R.
+      { induction x; try lra.
+        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
+          apply IZR_lt; lia.
+        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
+          apply IZR_lt; lia.
+      }
+      pose proof (H m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_neg_inv in Hs.
+      assert (forall x, IZR (Z.pos x) > 0)%R.
+      { induction x; try lra.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+      }
+      pose proof (H m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_pos_inv in Hs.
+      assert (forall x, IZR (Z.neg x) < 0)%R.
+      { induction x; try lra.
+        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
+          apply IZR_lt; lia.
+        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
+          apply IZR_lt; lia.
+      }
+      pose proof (H m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+  - apply do_overflow_false in Ho1.
+    unfold dont_overflow in Ho1.
+    rewrite <- Ex, <- Ey in *.
+    unfold R_imax in Ho1.
+    rewrite Ho1 in H.
+    now destruct H as [<- [Hf _]], (Bplus _ _ _).
+Qed.
 
 End Correction.
\ No newline at end of file
diff --git a/src_common/ieee/coq/Rextended.v b/src_common/ieee/coq/Rextended.v
index 05dd21241868d4c3796c41ba6fda614dda677707..a75e85c5dbe82b18b31f42d04be96eca34ee3534 100644
--- a/src_common/ieee/coq/Rextended.v
+++ b/src_common/ieee/coq/Rextended.v
@@ -199,6 +199,13 @@ Proof.
   now rewrite <- Raux.negb_Rlt_bool, H.
 Qed.
 
+Lemma do_overflow_true :
+  forall m r, do_overflow m r = true -> dont_overflow m r = false.
+Proof.
+  intros. unfold do_overflow, dont_overflow in *.
+  now rewrite <- Raux.negb_Rlt_bool, H.
+Qed.
+
 Lemma dont_overflow_true : 
   forall m r, dont_overflow m r = true -> do_overflow m r = false.
 Proof.
@@ -206,6 +213,13 @@ Proof.
   now rewrite <- Raux.negb_Rle_bool, Bool.negb_false_iff.
 Qed.
 
+Lemma dont_overflow_false : 
+  forall m r, dont_overflow m r = false -> do_overflow m r = true.
+Proof.
+  intros. unfold do_overflow, dont_overflow in *.
+  now rewrite <- Bool.negb_false_iff, Raux.negb_Rlt_bool.
+Qed.
+
 Lemma F2R_congr :
   forall m1 e1 m2 e2, m1 = m2 -> e1 = e2 ->
   @Defs.F2R Zaux.radix2 {| Defs.Fnum := m1; Defs.Fexp := e1 |} =