diff --git a/src_common/ieee/coq/Interval.v b/src_common/ieee/coq/Interval.v
index 243f26afa618f497e2b21f8c3c33bd85f1c919a3..f2351dbb68c78c96e4f2f026d26c34473f44e9d8 100644
--- a/src_common/ieee/coq/Interval.v
+++ b/src_common/ieee/coq/Interval.v
@@ -16,62 +16,62 @@ Context (Hemax : Prec_lt_emax prec emax).
 Definition float := binary_float prec emax.
 
 Inductive Interval_aux :=
-  | Aux_Bot : Interval_aux
-  | Aux_nan : Interval_aux
-  | Aux_intv : forall (l h : float) (nan : bool), Interval_aux.
+  | I_Bot : Interval_aux
+  | I_nan : Interval_aux
+  | I_intv : forall (l h : float) (nan : bool), Interval_aux.
 
 Definition contains (I : Interval_aux) (x : float) : Prop :=
   match I with
-  | Aux_Bot => False
-  | Aux_nan => x = NaN
-  | Aux_intv l h n =>
+  | I_Bot => False
+  | I_nan => is_nan x = true
+  | I_intv l h n =>
     l <= x <= h \/ (is_nan x && n = true)
   end.
 
 Definition containsb (I : Interval_aux) (x : float) : bool :=
   match I with
-  | Aux_Bot => true
-  | Aux_nan => is_nan x
-  | Aux_intv l h n =>
+  | I_Bot => true
+  | I_nan => is_nan x
+  | I_intv l h n =>
     (Bleb l x && Bleb x h) || (is_nan x && n)
   end.
 
 Definition Iadd_up_to_NaN (I1 I2 : Interval_aux) : bool :=
   match I1, I2 with
-  | Aux_Bot, _ => false
-  | _, Aux_Bot => false
-  | Aux_nan, _ => true
-  | _, Aux_nan => true
-  | Aux_intv l h n, Aux_intv l' h' n' =>
+  | I_Bot, _ => false
+  | _, I_Bot => false
+  | I_nan, _ => true
+  | _, I_nan => true
+  | I_intv l h n, I_intv l' h' n' =>
     n || n' || (containsb I1 +oo && containsb I2 -oo) || (containsb I1 -oo && containsb I2 +oo)
   end.
 
 Definition Iadd_aux (m : mode) (I1 I2 : Interval_aux) : Interval_aux :=
   match I1, I2 with
-  | Aux_Bot, _ => Aux_Bot
-  | _, Aux_Bot => Aux_Bot
-  | Aux_nan, _ => Aux_nan
-  | _, Aux_nan => Aux_nan
-  | Aux_intv l h n, Aux_intv l' h' n' =>
+  | I_Bot, _ => I_Bot
+  | _, I_Bot => I_Bot
+  | I_nan, _ => I_nan
+  | _, I_nan => I_nan
+  | I_intv l h n, I_intv l' h' n' =>
     let sum1 := Bplus m l l' in
     let sum2 := Bplus m h h' in
     match is_nan sum1 with
     | true =>
       match is_nan sum2 with
-      | true => Aux_nan
-      | false => Aux_intv +oo +oo true
+      | true => I_nan
+      | false => I_intv +oo +oo true
       end
     | false =>
       match is_nan sum2 with
-      | true => Aux_intv -oo -oo true
-      | false => Aux_intv sum1 sum2 (Iadd_up_to_NaN I1 I2)
+      | true => I_intv -oo -oo true
+      | false => I_intv sum1 sum2 (Iadd_up_to_NaN I1 I2)
       end
     end
   end.
 
 Definition valid_interval (I : Interval_aux) : Prop :=
   match I with
-  | Aux_intv l h _ => l <= h
+  | I_intv l h _ => l <= h
   | _ => True
   end.
 
@@ -89,9 +89,15 @@ Proof.
 Qed.
 
 
-
 Definition Interval := { I : Interval_aux | valid_interval I }.
 
+Program Definition Iadd (m : mode) (I1 I2 : Interval) : Interval :=
+  Iadd_aux m I1 I2.
+Next Obligation.
+  apply valid_interval_Iadd;
+  now destruct I1, I2.
+Defined.
+
 Lemma Bplus_nan_inv :
   forall (m : mode) (x y:float), is_nan (Bplus m x y) = true ->
   x = +oo /\ y = -oo \/ x = -oo /\ y = +oo \/ x = NaN \/ y = NaN.
@@ -110,14 +116,13 @@ Proof.
 Qed.
 
 Program Lemma Iadd_correct :
-  forall m (I1 I2 : Interval) (x y : float), contains I1 x -> contains I2 y -> contains (Iadd_aux m I1 I2) (Bplus m x y).
+  forall m (I1 I2 : Interval) (x y : float), contains I1 x -> contains I2 y -> contains (Iadd m I1 I2) (Bplus m x y).
 Proof.
-  intros m I1 I2 x y Hx Hy; 
-  destruct I1 as [[ | | l h n ] H1] eqn:EI1, I2 as [[ | | l' h' n' ] H2] eqn:EI2;
+  intros m [[ | | l h n ] H1] [[ | | l' h' n' ] H2] x y Hx Hy; 
   simpl in *; try easy.
-  - now rewrite Hx.
-  - now rewrite Hx.
   - now (fdestruct x; rewrite Hy).
+  - fdestruct x.
+  - fdestruct x; fdestruct y.
   - destruct (is_nan (Bplus m l l')) eqn:E1, (is_nan (Bplus m h h')) eqn:E2; intuition.
   + destruct (Bplus_nan_inv _ _ _ E1); intuition; subst; try easy.
     * rewrite (infp_le_is_infp _ _ _ H0) in *.
@@ -171,6 +176,261 @@ Proof.
   + fdestruct y; fdestruct x; destruct n; simpl; intuition.
 Qed.
 
+Lemma Bleb_refl :
+  forall x:float, is_nan x = false -> Bleb x x = true.
+Proof.
+  intros x Hx; fdestruct x.
+  apply le_Bleb; auto; lra.
+Qed.
+
+Lemma Bleb_false_Bltb :
+  forall x y:float, is_nan x = false -> is_nan y = false -> Bleb x y = false -> Bltb y x = true.
+Proof.
+  intros x y Hx Hy Hxy.
+  destruct x as [ | [ ] | | ] eqn:Ex, y as [ | [ ] | | ] eqn:Ey; try easy; rewrite <- Ex, <- Ey in *;
+  unfold Bleb, SpecFloat.SFleb in Hxy;
+  replace (SpecFloat.SFcompare (B2SF _) (B2SF _)) with (Bcompare x y) in Hxy by auto;
+  assert (Fx: is_finite x = true) by (rewrite Ex; auto);
+  assert (Fy: is_finite y = true) by (rewrite Ey; auto);
+  rewrite (Bcompare_correct _ _ x y Fx Fy) in Hxy; auto;
+  destruct (Raux.Rcompare _ _) eqn:E; try easy;
+  apply Raux.Rcompare_Gt_inv in E;
+  apply lt_Bltb; auto.
+Qed.
+
+Definition Bmax (f1 f2 : float) : float :=
+  if is_nan f1 || is_nan f2 then NaN
+  else if Bleb f1 f2 then f2
+  else f1.
+
+Definition Bmin (f1 f2 : float) : float :=
+  if is_nan f1 || is_nan f2 then NaN
+  else if Bleb f1 f2 then f1
+  else f2.
+
+Lemma Bmax_max_1 :
+  forall x y, (Bmax x y = x \/ Bmax x y = y).
+Proof.
+  intros [ ] [ ]; unfold Bmax; destruct Bleb; intuition.
+Qed.
+
+Lemma Bltb_Bleb :
+  forall x y : float, Bltb x y  = true -> Bleb x y = true.
+Proof.
+  intros x y Hxy.
+  fdestruct x; fdestruct y;
+  apply le_Bleb; auto;
+  apply Bltb_lt in Hxy; auto;
+  lra.
+Qed.
+
+Lemma Bmax_max_2 :
+  forall x y, is_finite x = true -> is_finite y = true -> x <= Bmax x y  /\ y <= Bmax x y.
+Proof.
+  intros x y Fx Fy; unfold Bmax.
+  assert (HnanX: is_nan x = false) by fdestruct x.
+  assert (HnanY: is_nan y = false) by fdestruct y.
+  rewrite HnanX, HnanY; simpl.
+  split.
+  - destruct (Bleb x y) eqn:?; auto.
+    apply Bleb_refl; fdestruct x.
+  - destruct (Bleb x y) eqn:E.
+    + apply Bleb_refl; fdestruct y.
+    + apply Bleb_false_Bltb in E; auto.
+      now apply Bltb_Bleb in E.
+Qed.
+
+Lemma Bmax_le :
+  forall x y z : float, x <= z -> y <= z -> Bmax x y <= z.
+Proof.
+  intros x y z Hxz Hyz.
+  assert (HnanX: is_nan x = false) by fdestruct x.
+  assert (HnanY: is_nan y = false) by fdestruct y.
+  unfold Bmax.
+  rewrite HnanX, HnanY; simpl.
+  now destruct (Bleb x y).
+Qed.
+
+Lemma Bmax_not_nan_inv :
+  forall x y, is_nan (Bmax x y) = false -> is_nan x = false /\ is_nan y = false.
+Proof.
+  intros; split.
+  + fdestruct x.
+  + fdestruct x; fdestruct y.
+Qed.
+
+Lemma Bmin_not_nan_inv :
+  forall x y, is_nan (Bmin x y) = false -> is_nan x = false /\ is_nan y = false.
+Proof.
+  intros; split.
+  + fdestruct x.
+  + fdestruct x; fdestruct y.
+Qed.
+
+Lemma Bmax_le_inv :
+  forall x y z : float, Bmax x y <= z -> x <= z /\ y <= z.
+Proof.
+  intros x y z Hxyz.
+  assert (is_nan (Bmax x y) = false) by (fdestruct (Bmax x y)).
+  unfold Bmax in Hxyz.
+  apply Bmax_not_nan_inv in H.
+  destruct H as [H1 H2].
+  rewrite H1, H2 in Hxyz.
+  simpl in *.
+  destruct (Bleb x y) eqn:E; split; auto.
+  - now apply (Bleb_trans _ _ x y z).
+  - apply Bleb_false_Bltb in E; auto.
+    apply Bltb_Bleb in E; auto.
+    now apply (Bleb_trans _ _ y x z).
+Qed.
+
+Lemma Bmin_min_1 :
+  forall x y, (Bmin x y = x \/ Bmin x y = y).
+Proof.
+  intros [ ] [ ]; unfold Bmin; destruct Bleb; intuition.
+Qed.
+
+Lemma Bmin_min_2 :
+  forall x y, is_finite x = true -> is_finite y = true -> Bmin x y <= x /\ Bmin x y <= y.
+Proof.
+  intros x y Fx Fy; unfold Bmin.
+  assert (HnanX: is_nan x = false) by fdestruct x.
+  assert (HnanY: is_nan y = false) by fdestruct y.
+  rewrite HnanX, HnanY; simpl.
+  split.
+  - destruct (Bleb x y) eqn:?.
+    + apply Bleb_refl; fdestruct x.
+    + assert (Hx : is_nan x = false) by (fdestruct x).
+      assert (Hy : is_nan y = false) by (fdestruct y).
+      apply Bleb_false_Bltb in Heqb; auto.
+      apply Bltb_lt in Heqb; auto.
+      apply le_Bleb; auto.
+      lra.
+  - destruct (Bleb x y) eqn:E; auto.
+    apply Bleb_refl; fdestruct y.
+Qed.
+
+Lemma Bmin_le :
+  forall x y z : float, z <= x -> z <= y -> z <= Bmin x y.
+Proof.
+  intros x y z Hxz Hyz.
+  assert (HnanX: is_nan x = false) by (fdestruct z; fdestruct x).
+  assert (HnanY: is_nan y = false) by (fdestruct z; fdestruct y).
+  unfold Bmin.
+  rewrite HnanX, HnanY; simpl.
+  now destruct (Bleb x y).
+Qed.
+
+Lemma Bmin_le_inv :
+  forall x y z : float, z <= Bmin x y -> z <= x /\ z <= y.
+Proof.
+  intros x y z Hxyz.
+  assert (is_nan (Bmin x y) = false) by (fdestruct (Bmin x y); fdestruct z).
+  unfold Bmin in Hxyz.
+  apply Bmin_not_nan_inv in H.
+  destruct H as [H1 H2].
+  rewrite H1, H2 in Hxyz.
+  simpl in *.
+  destruct (Bleb x y) eqn:E; split; auto.
+  - now apply (Bleb_trans _ _ z x y).
+  - apply Bleb_false_Bltb in E; auto.
+    apply Bltb_Bleb in E.
+    now apply (Bleb_trans _ _ z y x).
+Qed.
+
+Definition inter_aux (I1 I2 : Interval_aux) : Interval_aux :=
+  match I1, I2 with
+  | I_Bot, _ => I_Bot
+  | _, I_Bot => I_Bot
+  | I_nan, I_nan => I_nan
+  | I_nan, I_intv _ _ b => if b then I_nan else I_Bot
+  | I_intv _ _ b, I_nan => if b then I_nan else I_Bot
+  | I_intv l h b, I_intv l' h' b' =>
+    if Bleb h l' || Bleb h' l then 
+      if (b && b') then I_nan else I_Bot 
+    else I_intv (Bmax l l') (Bmin h h') (b && b')
+  end.
+
+
+Lemma valid_interval_inter :
+  forall I1 I2, valid_interval I1 -> valid_interval I2 -> valid_interval (inter_aux I1 I2).
+Proof.
+  intros [ | | l h ] [ | | l' h'] H1 H2; simpl in *; try easy.
+  + now destruct nan.
+  + now destruct nan.
+  + destruct (Bleb h l') eqn:Hhl'; simpl; try (now destruct nan, nan0).
+    destruct (Bleb h' l) eqn:Hh'l; simpl; try (now destruct nan, nan0).
+    apply Bleb_false_Bltb in Hh'l.
+    apply Bleb_false_Bltb in Hhl'.
+    - destruct (Bmax_max_1 l l') as [-> | ->];
+      destruct (Bmin_min_1 h h') as [-> | ->]; auto.
+      * now apply Bltb_Bleb in Hh'l.
+      * now apply Bltb_Bleb in Hhl'.
+    - fdestruct h; fdestruct l.
+    - fdestruct l'.
+    - fdestruct h'; fdestruct l'.
+    - fdestruct l.
+Qed.
+
+Program Definition inter (I1 I2 : Interval) : Interval :=
+  inter_aux I1 I2.
+Next Obligation.
+  destruct I1, I2; simpl.
+  now apply valid_interval_inter.
+Defined.
+
+Compute (inter_aux (I_intv (-oo) (-oo) true) (I_intv (+oo) (+oo) true)).
+
+Program Lemma inter_correct_l :
+  forall I1 I2, forall x, contains (inter I1 I2) x -> contains I1 x.
+Proof.
+  intros [ [ | | ? ? [ ]] H1 ] [ [ | | ? ? [ ]] H2 ] x Hx; simpl in *; try easy.
+  - intuition.
+  - destruct (Bleb h l0), (Bleb h0 l); simpl in *; try (rewrite Hx; intuition).
+    destruct Hx as [ [Hc1 Hc2] | ]; auto; left; split.
+    + now apply Bmax_le_inv in Hc1.
+    + now apply Bmin_le_inv in Hc2.  
+  - destruct (Bleb h l0) eqn:E1, (Bleb h0 l) eqn:E2; simpl in *; auto.
+    destruct Hx as [ [ Hc1 Hc2 ] |  ]; auto; left; split.
+    + apply Bmax_le_inv in Hc1; intuition.
+    + apply Bmin_le_inv in Hc2; intuition.
+    + fdestruct x.
+    + fdestruct x.
+  - destruct (Bleb h l0) eqn:E1, (Bleb h0 l) eqn:E2; simpl in *; auto.
+    destruct Hx as [ [ Hc1 Hc2 ] |  ]; auto; left; split.
+    + apply Bmax_le_inv in Hc1; intuition.
+    + apply Bmin_le_inv in Hc2; intuition.
+  - destruct (Bleb h l0) eqn:E1, (Bleb h0 l) eqn:E2; simpl in *; auto.
+    destruct Hx as [ [ Hc1 Hc2 ] |  ]; auto; left; split.
+    + apply Bmax_le_inv in Hc1; intuition.
+    + apply Bmin_le_inv in Hc2; intuition.
+Qed.
+
+Program Lemma inter_correct_r :
+  forall I1 I2, forall x, contains (inter I1 I2) x -> contains I2 x.
+Proof.
+  intros [ [ | | ? ? [ ]] H1 ] [ [ | | ? ? [ ]] H2 ] x Hx; simpl in *; try easy.
+  - rewrite Hx; intuition.
+  - destruct (Bleb h l0), (Bleb h0 l); simpl in *; try (rewrite Hx; intuition).
+    destruct Hx as [ [Hc1 Hc2] | ]; auto; left; split.
+    + now apply Bmax_le_inv in Hc1.
+    + now apply Bmin_le_inv in Hc2.
+  - destruct (Bleb h l0), (Bleb h0 l); simpl in *; try easy.
+    destruct Hx as [ [Hc1 Hc2] | ]; auto; left; split.
+    + now apply Bmax_le_inv in Hc1.
+    + now apply Bmin_le_inv in Hc2.
+  - destruct (Bleb h l0), (Bleb h0 l); simpl in *; try easy.
+    destruct Hx as [ [Hc1 Hc2] | ]; auto; left; split.
+    + now apply Bmax_le_inv in Hc1.
+    + now apply Bmin_le_inv in Hc2.
+    + fdestruct x.
+    + fdestruct x.
+  - destruct (Bleb h l0), (Bleb h0 l); simpl in *; try easy.
+    destruct Hx as [ [Hc1 Hc2] | ]; auto; left; split.
+    + now apply Bmax_le_inv in Hc1.
+    + now apply Bmin_le_inv in Hc2.
+Qed.
+
 Ltac classify_nan x :=
   match goal with
   | [ H : is_nan x = true |- _ ] =>
diff --git a/src_common/ieee/coq/Rextended.v b/src_common/ieee/coq/Rextended.v
index af26311fde27c3f8bb1850ded07b1bee0737c7e0..0a84bffab8d4b9d56ccfc5a9d70e24bdba15cf9a 100644
--- a/src_common/ieee/coq/Rextended.v
+++ b/src_common/ieee/coq/Rextended.v
@@ -122,6 +122,22 @@ Proof.
   apply Raux.Rcompare_Gt_inv in E; lra.
 Qed.
 
+Lemma lt_Bltb :
+  forall (x y : float),
+    is_finite x = true ->
+    is_finite y = true ->
+    (B2R x < B2R y)%R ->
+    Bltb x y = true.
+Proof.
+  intros x y Fx Fy Hxy.
+  unfold Bltb, SpecFloat.SFltb.
+  replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) by auto.
+  rewrite (Bcompare_correct _ _ x y Fx Fy).
+  destruct Raux.Rcompare eqn:E; auto.
+  - apply Raux.Rcompare_Eq_inv in E; lra.
+  - apply Raux.Rcompare_Gt_inv in E; lra.
+Qed.
+
 Lemma F_fmax_max :
   forall (x : float), is_finite x = true -> Bleb x F_fmax = true. 
 Proof.
diff --git a/src_common/ieee/coq/Utils.v b/src_common/ieee/coq/Utils.v
index 7b03c20c9e3a132117b1b044908f4de074a8c3ce..3899ac9ec2a2394549a03681e69d023ea08ec557 100644
--- a/src_common/ieee/coq/Utils.v
+++ b/src_common/ieee/coq/Utils.v
@@ -136,7 +136,51 @@ Proof.
   - simpl; destruct m; reflexivity.
 Qed.
 
-Lemma Bplus_correct_full :
+Lemma Bleb_trans :
+  forall (x y z : float), x <= y -> y <= z -> x <= z.
+Proof.
+  intros x y z Hxy Hyz.
+  fdestruct x; fdestruct y; fdestruct z;
+  apply le_Bleb; auto;
+  apply Bleb_le in Hxy; auto;
+  apply Bleb_le in Hyz; auto;
+  lra.
+Qed.
+
+Lemma Bltb_trans :
+  forall (x y z : float), Bltb x y = true -> Bltb y z = true -> Bltb x z = true.
+Proof.
+  intros x y z Hxy Hyz.
+  fdestruct x; fdestruct y; fdestruct z;
+  apply lt_Bltb; auto;
+  apply Bltb_lt in Hxy; auto;
+  apply Bltb_lt in Hyz; auto;
+  lra.
+Qed.
+
+Lemma Bltb_Bleb_trans :
+  forall x y z : float, Bltb x y = true -> y <= z -> Bltb x z = true.
+Proof.
+  intros x y z Hxy Hyz.
+  fdestruct x; fdestruct y; fdestruct z;
+  apply lt_Bltb; auto;
+  apply Bltb_lt in Hxy; auto;
+  apply Bleb_le in Hyz; auto;
+  lra.
+Qed.
+
+Lemma Bleb_Bltb_trans :
+  forall x y z : float, Bleb x y = true -> Bltb y z = true -> Bltb x z = true.
+Proof.
+  intros x y z Hxy Hyz.
+  fdestruct x; fdestruct y; fdestruct z;
+  apply lt_Bltb; auto;
+  apply Bleb_le in Hxy; auto;
+  apply Bltb_lt in Hyz; auto;
+  lra.
+Qed.
+
+(* Lemma Bplus_correct_full :
   forall (m : mode) (x y : float),
   is_nan (Bplus m x y) = false ->
   B2Rx (Bplus m x y) = round m (add (B2Rx x) (B2Rx y)).
@@ -172,7 +216,7 @@ Proof.
     apply round_id.
   - Check (Bplus_correct).
   admit.
-Admitted.
+Admitted. *)
 
 End Utils.