for n, i being Nat holds
( cos (((2 * PI) * i) / n) = cos (((2 * PI) * (i mod n)) / n) & sin (((2 * PI) * i) / n) = sin (((2 * PI) * (i mod n)) / n) )