diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 6e35c2f0467979bd71379cf0b39d9e22f68eae5b..5f8bbf140583beae44e2abfedd73922941d8e8e1 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -40,8 +40,9 @@ Inductive is_false: val -> type -> Prop :=
       is_false (Vint Int.zero) (Tint sz sg)
   | is_false_pointer: forall t,
       is_false (Vint Int.zero) (Tpointer t)
- | is_false_float: forall sz,
-      is_false (Vfloat Float.zero) (Tfloat sz).
+ | is_false_float: forall sz f,
+      Float.cmp Ceq f Float.zero = true ->
+      is_false (Vfloat f) (Tfloat sz).
 
 Inductive is_true: val -> type -> Prop :=
   | is_true_int_int: forall n sz sg,
@@ -55,7 +56,7 @@ Inductive is_true: val -> type -> Prop :=
   | is_true_pointer_pointer: forall b ofs t,
       is_true (Vptr b ofs) (Tpointer t)
  | is_true_float: forall f sz,
-      f <> Float.zero ->
+      Float.cmp Ceq f Float.zero = false ->
       is_true (Vfloat f) (Tfloat sz).
 
 Inductive bool_of_val : val -> type -> val -> Prop :=
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index 3f0f4b3ee92028bfea47d83df0b2acaaa4cb5ce3..e58570b623d3d7332e01a3a434608b6006f33568 100644
--- a/cfrontend/Cshmgenproof2.v
+++ b/cfrontend/Cshmgenproof2.v
@@ -78,10 +78,8 @@ Proof.
   try (exists v; intuition; inversion VTRUE; simpl; auto; fail).
   exists Vtrue; split.
   eapply eval_Ebinop; eauto with cshm. 
-  inversion VTRUE; simpl. 
-  replace (Float.cmp Cne f0 Float.zero) with (negb (Float.cmp Ceq f0 Float.zero)).
-  rewrite Float.eq_zero_false. reflexivity. auto.
-  rewrite Float.cmp_ne_eq. auto.
+  inversion VTRUE; simpl.
+  rewrite Float.cmp_ne_eq. rewrite H1. auto.
   apply Vtrue_is_true.
 Qed.
 
@@ -98,10 +96,8 @@ Proof.
   try (exists v; intuition; inversion VFALSE; simpl; auto; fail).
   exists Vfalse; split.
   eapply eval_Ebinop; eauto with cshm. 
-  inversion VFALSE; simpl. 
-  replace (Float.cmp Cne Float.zero Float.zero) with (negb (Float.cmp Ceq Float.zero Float.zero)).
-  rewrite Float.eq_zero_true. reflexivity. 
-  rewrite Float.cmp_ne_eq. auto.
+  inversion VFALSE; simpl.
+  rewrite Float.cmp_ne_eq. rewrite H1. auto.
   apply Vfalse_is_false.
 Qed.
 
diff --git a/lib/Floats.v b/lib/Floats.v
index 50298f7071e77af2e8600abcc3b2779a99373be0..5c20cdd637c6731bf6ef83d7c73b78372178a7ac 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -70,9 +70,6 @@ Axiom cmp_le_lt_eq:
 Axiom cmp_ge_gt_eq:
   forall f1 f2, cmp Cge f1 f2 = cmp Cgt f1 f2 || cmp Ceq f1 f2.
 
-Axiom eq_zero_true: cmp Ceq zero zero = true.
-Axiom eq_zero_false: forall f, f <> zero -> cmp Ceq f zero = false.
-
 Axiom bits_of_double_of_bits:
   forall n, bits_of_double (double_of_bits n) = n.
 Axiom double_of_bits_of_double: