theorem :: SIN_COS5:37

for x being Real st (exp_R x) - (exp_R (- x)) <> 0 holds
(tanh x) * (coth x) = 1