Definition isU16 (z : Z) : Prop :=
  (u16Min <= z) /\ (z <= u16Max).
