Definition isU8 (z : Z) : Prop :=
  (u8Min <= z) /\ (z <= u8Max).
