diff --git a/src_common/ieee/coq/.nra.cache b/src_common/ieee/coq/.nra.cache
index 1e48d00680c8db820e245fdf2ea46806e94456c1..ddc240ee3583d254990ee9fa18e1ff3d2d5b7431 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 2f67e802709a915931b34598981858df1a7a908e..16ad45b4a9da1e644c0bdc7e93c1c29c78439580 100644
--- a/src_common/ieee/coq/Correction_thms.v
+++ b/src_common/ieee/coq/Correction_thms.v
@@ -231,4 +231,79 @@ Proof.
     now destruct H as [<- [Hf _]], (Bplus _ _ _).
 Qed.
 
+Theorem Bplus_le_compat:
+  forall m (a b c : float),
+    is_nan (Bplus m a c) = false ->
+    is_nan (Bplus m b c) = false ->
+    a <= b ->
+    Bplus m a c <= Bplus m b c.
+Proof.
+  intros m a b c Hnan1 Hnan2 Hab.
+  apply B2Rx_le; try easy.
+  rewrite (Bplus_correct m a c Hnan1).
+  rewrite (Bplus_correct m b c Hnan2).
+  apply round_le.
+  apply add_leb_compat.
+  fdestruct a; fdestruct b; simpl.
+  - apply Raux.Rle_bool_true; lra.
+  - apply Raux.Rle_bool_true; lra.
+  - destruct s; simpl; try easy.
+    unfold Defs.F2R; simpl.
+    apply Raux.Rle_bool_true.
+    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 m0).
+    pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+    nra.
+  - apply Raux.Rle_bool_true; lra.
+  - apply Raux.Rle_bool_true; lra.
+  - destruct s; simpl; try easy.
+    unfold Defs.F2R; simpl.
+    apply Raux.Rle_bool_true.
+    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 m0).
+    pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+    nra.
+  - destruct s; simpl; try easy.
+    unfold Defs.F2R; simpl.
+    apply Raux.Rle_bool_true.
+    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 m0).
+    pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+    nra.
+  - destruct s; simpl; try easy.
+    unfold Defs.F2R; simpl.
+    apply Raux.Rle_bool_true.
+    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 m0).
+    pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+    nra.
+  - destruct s, s0; simpl; try easy;
+      apply Bleb_le in Hab; auto;
+      now apply Raux.Rle_bool_true.
+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 a75e85c5dbe82b18b31f42d04be96eca34ee3534..3fda6b8649a01d01301249ce75978430fa030e47 100644
--- a/src_common/ieee/coq/Rextended.v
+++ b/src_common/ieee/coq/Rextended.v
@@ -580,6 +580,24 @@ Definition add (x y : Rx) : Rx :=
     end
   end.
 
+Lemma add_leb_compat :
+  forall x y z : Rx,
+  leb x y = true -> leb (add x z) (add y z) = true.
+Proof.
+  intros [ ] [ ] [ ] H.
+  - simpl in *.
+    apply Rle_le in H.
+    apply Raux.Rle_bool_true.
+    lra.
+  - now destruct b.
+  - now destruct b.
+  - now destruct b, b0.
+  - now destruct b.
+  - now destruct b, b0.
+  - now destruct b, b0.
+  - now destruct b, b0, b1.
+Qed.
+
 Lemma add_real :
   forall (r1 r2 : R), add (Real r1) (Real r2) = Real (r1 + r2)%R.
 Proof. reflexivity. Qed.
@@ -698,6 +716,7 @@ Qed.
 End Rextended.
 
 Arguments round {prec} {emax} {Hprec} {Hemax}.
+Arguments round_le {prec} {emax} {Hprec} {Hemax}.
 Arguments B2Rx {prec} {emax}.
 Arguments B2Rx_le {prec} {emax}.
 Arguments le_B2Rx {prec} {emax}.