thus (0 + (u * z)) mod z = 0 mod z by NAT_D:61
.= 0 ; :: thesis: verum