1 < n by NAT_2:19, NAT_2:def 1;
then 0. (Z/ n) = 0 by Th4;
hence not Z/ n is flat by Th17; :: thesis: verum