Definition u32Min : Z := 0.
