diff --git a/src_common/ieee/coq/.nra.cache b/src_common/ieee/coq/.nra.cache
index ddc240ee3583d254990ee9fa18e1ff3d2d5b7431..a3ffd9207cbe64a8ee0e7dcb6a377133632e88ac 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 16ad45b4a9da1e644c0bdc7e93c1c29c78439580..29969ef9ad64be112e2ba5de0e867abd6adb7a4d 100644
--- a/src_common/ieee/coq/Correction_thms.v
+++ b/src_common/ieee/coq/Correction_thms.v
@@ -55,52 +55,25 @@ Proof.
       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.
+      pose proof (IZR_pos m2); pose proof (IZR_pos 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.
+      pose proof (IZR_neg m2); pose proof (IZR_neg 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.
+      pose proof (IZR_pos m2); pose proof (IZR_pos 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.
@@ -109,120 +82,58 @@ Proof.
       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.
+      pose proof (IZR_pos m2); pose proof (IZR_pos 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.
+      pose proof (IZR_pos m2); pose proof (IZR_pos 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).
+      pose proof (IZR_neg m2); pose proof (IZR_neg m3);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5);
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
       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.
+      pose proof (IZR_pos m2); pose proof (IZR_pos 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.
+      pose proof (IZR_neg m2); pose proof (IZR_neg 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.
+      pose proof (IZR_pos m2); pose proof (IZR_pos 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.
+      pose proof (IZR_neg m2); pose proof (IZR_neg 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 *.
@@ -250,14 +161,7 @@ Proof.
   - 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 (IZR_pos m0).
     pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
     nra.
   - apply Raux.Rle_bool_true; lra.
@@ -265,40 +169,19 @@ Proof.
   - 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 (IZR_pos 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 (IZR_neg 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 (IZR_neg m0).
     pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
     nra.
   - destruct s, s0; simpl; try easy;
diff --git a/src_common/ieee/coq/Rextended.v b/src_common/ieee/coq/Rextended.v
index 3fda6b8649a01d01301249ce75978430fa030e47..f15c5136b161398deaf694cfa03def1f4e3499e0 100644
--- a/src_common/ieee/coq/Rextended.v
+++ b/src_common/ieee/coq/Rextended.v
@@ -42,6 +42,22 @@ Proof.
   intros; lra.
 Qed.
 
+Lemma IZR_neg :
+  (forall x, IZR (Z.neg x) < 0)%R.
+Proof.
+  induction x; try lra;
+  apply (Rgt_trans _ (IZR (Z.neg x))); auto;
+  apply IZR_lt; lia.
+Qed.
+
+Lemma IZR_pos :
+  (forall x, IZR (Z.pos x) > 0)%R.
+Proof.
+  induction x; try lra;
+  apply (Rgt_trans _ (IZR (Z.pos x))); auto;
+  apply IZR_lt; lia.
+Qed.
+
 End Rutils.