theorem :: SIN_COS8:15

for y, z being Real holds ((cosh y) + (cosh z)) / ((cosh y) - (cosh z)) = (coth ((y + z) / 2)) * (coth ((y - z) / 2))