for x being Real st sin . x <> 0 holds
( cos / sin is_differentiable_in x & diff ((cos / sin),x) = - (1 / ((sin . x) ^2)) )