theorem :: SIN_COS9:4

( cot is_differentiable_on ].0,PI.[ & ( for x being Real st x in ].0,PI.[ holds
diff (cot,x) = - (1 / ((sin . x) ^2)) ) ) by Lm2, Lm4;