Definition u16Max : Z := (2 ^ 16) - 1.
