theorem :: SIN_COS5:41

for x1, x2 being Real st sinh x1 <> 0 & sinh x2 <> 0 holds
coth (x1 - x2) = (1 - ((coth x1) * (coth x2))) / ((coth x1) - (coth x2))