let x be Real; :: thesis: ( x in ].0,PI.[ implies diff (cot,x) = - (1 / ((sin . x) ^2)) )
assume x in ].0,PI.[ ; :: thesis: diff (cot,x) = - (1 / ((sin . x) ^2))
then sin . x <> 0 by COMPTRIG:7;
hence diff (cot,x) = - (1 / ((sin . x) ^2)) by FDIFF_7:47; :: thesis: verum