Definition u64Max : Z := (2 ^ 64) - 1.
