Axiom float16BitsRange : forall (r : R),
  u16Min <= float16BitsOf r /\ float16BitsOf r <= u16Max.
