diff --git a/src/number.rs b/src/number.rs
index b0abdbf..10392ef 100644
--- a/src/number.rs
+++ b/src/number.rs
@@ -90,10 +90,10 @@ pub open spec fn float_to_small_int(value: f64) -> Option<int>
 {
     if !value.is_finite_spec() ||
        !spec_f64_fract(value).eq_spec(&0.0f64) ||
-       spec_f64_abs(value).is_gt(&9_007_199_254_740_992.0) {
+       spec_f64_abs(value) > 9_007_199_254_740_992.0 {
         None
     }
-    else if value.is_ge(&0.0) {
+    else if value >= 0.0 {
         if ieee_float_cast::<u64, f64>(ieee_float_cast::<f64, u64>(value)).eq_spec(&value) {
             Some(ieee_float_cast::<f64, u64>(value) as int)
         }
@@ -285,6 +285,7 @@ impl Number {
             axiom_f64_obeys_eq_spec();
             axiom_f64_obeys_partial_cmp_spec();
             axiom_f64_ops_deterministic();
+            axiom_f64_comparisons_match_ieee();
         }
 
         if !value.is_finite() || value.fract() != 0.0 {
diff --git a/src/verusspec/float.rs b/src/verusspec/float.rs
index cdc412b..6ab6a44 100644
--- a/src/verusspec/float.rs
+++ b/src/verusspec/float.rs
@@ -14,6 +14,10 @@
 
 #[cfg(verus_keep_ghost)]
 use vstd::float::*;
+#[cfg(verus_keep_ghost)]
+use vstd::std_specs::cmp::PartialEqIs;
+#[cfg(verus_keep_ghost)]
+use vstd::std_specs::cmp::PartialOrdIs;
 use vstd::prelude::*;
 
 verus! {
@@ -28,6 +32,14 @@ pub axiom fn axiom_f64_obeys_partial_cmp_spec()
         <f64 as vstd::std_specs::cmp::PartialOrdSpec>::obeys_partial_cmp_spec(),
 ;
 
+pub axiom fn axiom_f64_comparisons_match_ieee()
+    ensures
+        forall|f1: f64, f2: f64| #[trigger] f1.ieee_lt(f2) <==> f1.is_lt(&f2),
+        forall|f1: f64, f2: f64| #[trigger] f1.ieee_le(f2) <==> f1.is_le(&f2),
+        forall|f1: f64, f2: f64| #[trigger] f1.ieee_gt(f2) <==> f1.is_gt(&f2),
+        forall|f1: f64, f2: f64| #[trigger] f1.ieee_ge(f2) <==> f1.is_ge(&f2),
+;
+
 pub axiom fn axiom_f64_ops_deterministic()
     ensures
         <f64 as vstd::std_specs::ops::NegSpec>::obeys_neg_spec(),