let a be positive light Real; :: thesis: 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)
let n be positive heavy Real; :: thesis: ((1 + a) to_power n) / (1 + (a to_power n)) < (1 - (a to_power n)) / ((1 - a) to_power n)
((1 + a) to_power n) * ((1 - a) to_power n) < (1 + (a to_power n)) * (1 - (a to_power n)) by IL1;
hence ((1 + a) to_power n) / (1 + (a to_power n)) < (1 - (a to_power n)) / ((1 - a) to_power n) by XREAL_1:106; :: thesis: verum