for x being Real st x ^2 > 1 holds
coth" x = tanh" (1 / x)