theorem Th72: :: SIN_COS9:72

arccot is_differentiable_on cot .: ].0,PI.[