theorem Th28: :: BASEL_2:28

for m being Nat holds Sum (sqr (cot (x_r-seq m))) = ((2 * m) * ((2 * m) - 1)) / 6