:: deftheorem defines coth" SIN_COS7:def 5 :
for x being Real holds coth" x = (1 / 2) * (log (number_e,((x + 1) / (x - 1))));