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