:: deftheorem defines coth SIN_COS5:def 1 :
for x being Real holds coth x = (cosh x) / (sinh x);