diff --git a/src_common/ieee/coq/Futils.v b/src_common/ieee/coq/Futils.v
index ac42095485e80e8dc0d9279074fde4864323b452..b4d7403488aff34778f329dd7f1b6d85db9645bb 100644
--- a/src_common/ieee/coq/Futils.v
+++ b/src_common/ieee/coq/Futils.v
@@ -77,6 +77,12 @@ Definition dont_overflow (x y : binary_float prec emax) (m : mode) :=
   let rsum := Generic_fmt.round Zaux.radix2 fexp (round_mode m) (B2R x + B2R y) in
   Raux.Rlt_bool (Rabs rsum) fmax = true.
 
+Definition do_overflow (x y : binary_float prec emax) (m : mode) := 
+  let fexp := @SpecFloat.fexp prec emax in
+  let fmax := Raux.bpow Zaux.radix2 emax in
+  let rsum := Generic_fmt.round Zaux.radix2 fexp (round_mode m) (B2R x + B2R y) in
+  Raux.Rlt_bool (Rabs rsum) fmax = false.
+
 Lemma Fadd_le_compat_aux:
   forall m w x y z H1 H2,
     is_finite w = true ->
@@ -112,6 +118,66 @@ Proof.
   intuition.
 Qed.
 
+Lemma add_nan :
+  forall m x y H1 H2,
+  is_finite x = true ->
+  is_finite y = true ->
+  is_nan (@Bplus prec emax H1 H2 m x y) = false.
+Proof.
+  intros m [[ ] | [ ] | | ] [ [ ] | [ ] | | ] H1 H2 Fx Fy; try easy.
+  - now destruct m.
+  - now destruct m.
+  - unfold Bplus; auto using is_nan_binary_normalize.
+Qed.
+
+Lemma Rlt_bool_Rcompare :
+  forall x y, Raux.Rlt_bool x y = true -> Raux.Rcompare x y = Lt.
+Proof.
+  intros; unfold Raux.Rlt_bool in *.
+  now destruct Raux.Rcompare eqn:E.
+Qed.
+
+Lemma Rlt_bool_inv :
+  forall x y, Raux.Rlt_bool x y = true -> (x < y)%R.
+Proof.
+  auto using Rlt_bool_Rcompare, Raux.Rcompare_Lt_inv.
+Qed.
+
+Lemma no_overflow :
+  forall m x y x' y',
+  is_finite x = true ->
+  is_finite x' = true ->
+  is_finite y = true ->
+  is_finite y' = true ->
+  x <= x' ->
+  y <= y' ->
+  dont_overflow x' y' m ->
+  dont_overflow x y m.
+Proof.
+  intros m x y x' y' Fx Fx' Fy Fy' Hx Hy H. unfold dont_overflow in *.
+  apply Rlt_bool_inv in H.
+  apply Raux.Rlt_bool_true.
+  apply (Fle_Rle _ _ Fx Fx') in Hx.
+  apply (Fle_Rle _ _ Fy Fy') in Hy.
+  (* erewrite Generic_fmt.round_le in H. *)
+Admitted.
+
+(**
+
+IDEA : prove that if I1 & I2 bounds don't overflow when added, 
+then for any x in I1, y in I2, x + y don't overflow.
+
+Then, redefined I1 + I2 as : 
+
+if bounds of I1, I2 may overflow once added then 
+  set new bounds & flag accordingly (correction still to be proved)
+else
+  just add the bounds
+  correction proof: 
+  (1) if x in I1 & y in I2, then x + y dont overflow (to be proved) 
+  (1) if x in I1 & y in I2, then x + y dont overflow (to be proved) 
+*)
+
 Lemma Fadd_le_compat:
   forall m w x y z H1 H2,
     is_finite w = true ->