theorem :: DIFF_4:6

for x0, x1 being Real st x0 in dom cot & x1 in dom cot holds
[!(cot (#) cot),x0,x1!] = - ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1)))