theorem Th72: :: SIN_COS9:72
arccot is_differentiable_on cot .: ].0,PI.[