Axiom float64BitsRange : forall (r : R),
  u64Min <= float64BitsOf r /\ float64BitsOf r <= u64Max.
