theorem :: DIFF_4:9

for h, x being Real st x + (h / 2) in dom cot & x - (h / 2) in dom cot holds
(cD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2)