theorem :: SIN_COS8:8

for x being Real st x <> 0 holds
( exp_R x = ((coth (x / 2)) + 1) / ((coth (x / 2)) - 1) & exp_R (- x) = ((coth (x / 2)) - 1) / ((coth (x / 2)) + 1) )