theorem :: COMPLEX3:80

for a being positive light Real
for n being positive heavy Real holds ((1 + a) to_power n) / (1 + (a to_power n)) < (1 - (a to_power n)) / ((1 - a) to_power n)