Definition u32Max : Z := (2 ^ 32) - 1.
