Axiom float32BitsRange : forall (r : R),
  u32Min <= float32BitsOf r /\ float32BitsOf r <= u32Max.
