for i1, i being Integer st i divides i1 & i1 <> 0 holds
|.i.| <= |.i1.|