Axiom float64BitsOf : forall (r : R), Z.
