theorem :: SIN_COS5:45

for x being Real st sinh x <> 0 holds
coth (2 * x) = (1 + ((coth x) ^2)) / (2 * (coth x))