Definition u64Min : Z := 0.
