Definition isU64 (z : Z) : Prop :=
  (u64Min <= z) /\ (z <= u64Max).
