theorem :: DIFF_2:70
for x0, x1 being Real st x0 in dom cot & x1 in dom cot holds
[!cot,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1)))