theorem :: DIFF_4:8

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