theorem Th36: :: SIN_COS5:36

for x being Real holds
( coth x = ((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) & sech x = 2 / ((exp_R x) + (exp_R (- x))) & cosech x = 2 / ((exp_R x) - (exp_R (- x))) )