for r being Real holds
( tan r = (cot r) " & cot r = (tan r) " )