Char (Z/ n) <> 0 ;
hence not Z/ n is preordered by tchar; :: thesis: verum