diff --git a/src_common/ieee/coq/finterval.v b/src_common/ieee/coq/finterval.v
index 023419a50e6bc02b8fc47c2b6ddc8f403eae10f4..8d3e27755900548782c7ba3e4526224a003f5b47 100644
--- a/src_common/ieee/coq/finterval.v
+++ b/src_common/ieee/coq/finterval.v
@@ -306,36 +306,6 @@ Proof.
   auto using le_is_infm.
 Qed.
 
-Ltac idestruct x :=
-  destruct x as [?a ?b ?n];
-  destruct a as [ [ ] | [ ] | | ] eqn:?Ea;
-  destruct b as [ [ ] | [ ] | | ] eqn:?Eb;
-  destruct n as [ | ] eqn:?En;
-  simpl;
-  try easy.
-
-
-(* Definition Iadd2 (m : mode) (A B : Interval) : Interval :=
-  let (a1, b1) := (lo A, hi A) in
-  let (a2, b2) := (lo B, hi B) in
-  let a := Fadd m a1 a2 in
-  let b := Fadd m b1 b2 in
-  let nan := (nan A || nan B) in
-  match a1, b1, a2, b2 with
-  | -oo, +oo, -oo, +oo => MK_INTERVAL (-oo) (+oo) true
-  
-  | -oo, +oo, -oo, -oo
-  | -oo, -oo, -oo, +oo => MK_INTERVAL (-oo) (-oo) true
-  
-  | -oo, _, -oo, _ => MK_INTERVAL (-oo) b nan
-  
-  | +oo, +oo, +oo, +oo => MK_INTERVAL (+oo) (+oo) nan
-  
-  | +oo, +oo, -oo, -oo
-  | -oo, -oo, +oo, +oo => MK_INTERVAL (+oo) (-oo) true
-  | _, _, _, _ => A
-  end. *)
-
 Record Interval2 := MK_INTERVAL2 {
   lo2 : B32;
   hi2 : B32;
@@ -435,7 +405,6 @@ Proof.
   now intros [ [ ] | [ ] | | ] H.
 Qed.
 
-
 Ltac classify_nan x :=
   match goal with
   | [ H : is_nan x = true |- _ ] =>
@@ -454,56 +423,28 @@ Ltac classify_inf x :=
     rewrite (proj1 (is_infp_iff x) H) in * ||
     assert (Hx_infp : x = +oo) by now rewrite <- is_infp_iff
   | [ H : +oo <= x |- _ ] =>
-    rewrite (infp_le_is_infp _ H) in * ||
-    assert (Hx_infp : x = +oo) by apply (infp_le_is_infp _ H)
+    rewrite (infp_le_is_infp _ H) in *
   | [ H : is_infm x = true |- _ ] =>
-    rewrite (proj1 (is_infm_iff x) H) in * ||
-    assert (Hx_infm : x = -oo) by now rewrite <- is_infm_iff
+    rewrite (proj1 (is_infm_iff x) H) in *
   | [ H : x <= -oo |- _ ] =>
-    rewrite (le_infm_is_infm x H) in * ||
-    assert (Hx_infm : x = -oo) by apply (le_infm_is_infm _ H)
+    rewrite (le_infm_is_infm x H) in *
   | _ => fail "can't determine if" x "is +oo or -oo"
   end.
 
-Ltac classify x :=
-  match goal with
-  | [ H : _ <= x |- _ ] =>
-    assert (is_nan x = false) by apply (not_nan_comp _ _ H)
-  | [ H : x <= _ |- _ ] =>
-    assert (is_nan x = false) by apply (not_nan_comp2 _ _ H)
-  | [ H : is_nan x = true |- _ ] =>
-    assert (x = B754_nan) by now rewrite <- (is_nan_iff x)
-  | [ H : (is_nan x = true /\ _) |- _ ] =>
-    assert (x = B754_nan) by now rewrite <- (is_nan_iff x)
-  end.
-
-Ltac sanitize :=
-  match goal with
-  | [ H : andb _ _ = true |- _ ] =>
-    rewrite Bool.andb_true_iff in H; destruct H;
-    sanitize
-  | [ H : _ /\ _ |- _ ] =>
-    destruct H; sanitize
-  | _ => idtac
-  end.
-
 Ltac feasy :=
   try easy;
     match goal with
-    | |- is_nan ?x = false => classify x; (try easy; intuition)
-    | |- is_finite ?x = true => classify x; (try easy; intuition)
+    | |- is_nan ?x = false => classify_nan x; (try easy; intuition)
     end.
 
 Ltac auto_contain :=
-  try easy; intuition; (right; simpl; intuition); (left; simpl; intuition).
+  try easy; first [ progress (right; simpl; intuition) | progress (left; simpl; intuition) ].
 
 Lemma contains_nan :
   forall I, contains2 I B754_nan <-> nan2 I = true.
 Proof.
-  (* intros [ ? ? ? ? [ ] ]; simpl; split; intros. try auto_contain.
-  inversion H; auto_contain. *)
-  intros [ ? ? ? ? [ ] ]; simpl; split; intros; try auto_contain.
-  inversion H; auto_contain.
+  intros [ ? ? ? ? [ ] ]; simpl; split; intros; try auto_contain. 
+  inversion H; try easy; intuition.
 Qed.
 
 Ltac boolean :=
@@ -516,6 +457,21 @@ Ltac boolean :=
     replace x with true by boolean; boolean
   end.
 
+Ltac irewrite :=
+  match goal with
+  | [ H : infp2 _ = _ |- _ ] => rewrite H; irewrite
+  | [ H : infm2 _ = _ |- _ ] => rewrite H; irewrite
+  | [ H : nan2 _ = _ |- _ ] => rewrite H; irewrite
+  | _ => idtac
+  end.
+
+Ltac fdiscriminate x :=
+  (classify_inf x; discriminate) ||
+  (classify_nan x; discriminate).
+
+Ltac fdestruct x :=
+  destruct x as [ [ ] | [ ] | | ].
+
 Lemma Iadd2_correct :
   forall m ix iy x y, 
   check2 ix = true ->
@@ -526,48 +482,25 @@ Lemma Iadd2_correct :
 Proof.
   intros.
   checked2.
-  contained2; intuition.
-  + unfold Iadd2; left; split; simpl.
-    - apply Fadd_le_compat; feasy.
-    - apply Fadd_le_compat; feasy.
-  + classify_nan x; unfold Iadd2; rewrite H7; auto_contain.
-  + unfold Iadd2; rewrite H7; simpl.
-    classify_inf x.
-    destruct y as [ [ ] | [ ] | | ]; auto_contain.
-    classify_inf (lo2 iy); discriminate.
-  + unfold Iadd2; rewrite H7; simpl.
-    classify_inf x.
-    destruct y as [ [ ] | [ ] | | ]; auto_contain.
-    classify_inf (hi2 iy); discriminate.
-  + unfold Iadd2; rewrite H7.
-    classify_nan y.
-    destruct x as [ [ ] | [ ] | | ]; auto_contain.
+  contained2; intuition; unfold Iadd2; irewrite.
+  + left; split; simpl; apply Fadd_le_compat; feasy.
+  + classify_nan x; auto_contain.
+  + classify_inf x. fdestruct y; 
+    try fdiscriminate (lo2 iy); auto_contain.
+  + classify_inf x. fdestruct y;
+    try fdiscriminate (hi2 iy); auto_contain.
+  + classify_nan y; fdestruct x; auto_contain.
+  + classify_nan x; auto_contain.
+  + classify_nan y; fdestruct x; auto_contain.
+  + classify_nan y; fdestruct x; auto_contain.
+  + classify_inf y; fdestruct x; 
+    try fdiscriminate (lo2 ix); auto_contain.
+  + classify_inf y; fdestruct x; 
+    try fdiscriminate (hi2 ix); auto_contain.
+  + classify_nan x; auto_contain.
   + classify_nan x; auto_contain.
-    boolean.
-  + unfold Iadd2; rewrite H6; simpl.
-    classify_nan y;
-    destruct x as [ [ ] | [ ] | | ]; auto_contain.
-  + unfold Iadd2; rewrite H6; simpl.
-    classify_nan y; 
-    destruct x as [ [ ] | [ ] | | ]; auto_contain.
-  + unfold Iadd2; rewrite H7; simpl.
-    classify_inf y;
-    destruct x as [ [ ] | [ ] | | ]; auto_contain.
-    classify_inf (lo2 ix); discriminate.
-  + unfold Iadd2; rewrite H7; simpl.
-    classify_inf y;
-    destruct x as [ [ ] | [ ] | | ]; auto_contain.
-    classify_inf (hi2 ix); discriminate.
-  + unfold Iadd2; rewrite H6; simpl.
-    classify_nan x; auto_contain.
-  + unfold Iadd2; rewrite H6; simpl.
-    classify_nan x; auto_contain.
-  + unfold Iadd2; rewrite H6, H7; simpl.
-    classify_inf x; classify_inf y; auto_contain.
-  + unfold Iadd2; rewrite H6, H7; simpl.
-    classify_inf x; classify_inf y; auto_contain.
-  + unfold Iadd2; rewrite H6, H7; simpl.
-    classify_inf x; classify_inf y; auto_contain.
-  + unfold Iadd2; rewrite H6, H7; simpl.
-    classify_inf x; classify_inf y; auto_contain.
+  + classify_inf x; classify_inf y; auto_contain.
+  + classify_inf x; classify_inf y; auto_contain.
+  + classify_inf x; classify_inf y; auto_contain.
+  + classify_inf x; classify_inf y; auto_contain.
 Qed.
\ No newline at end of file