for th1, th2 being Real st sin ((th1 + th2) / 2) <> 0 holds
((sin th1) + (sin th2)) / ((cos th2) - (cos th1)) = cot ((th1 - th2) / 2)