for r being Real st 0 < r & r < PI holds
( arccot (cot . r) = r & arccot (cot r) = r )