for x being Real st x > 0 & x <= 1 holds
sech2" x = cosh2" (1 / x)