for L being positive-definite Z_Lattice
for v being Vector of L holds ||.v.|| >= 0