Definition isU32 (z : Z) : Prop :=
  (u32Min <= z) /\ (z <= u32Max).
