for a, n being positive heavy Real
for b being positive light Real holds
( ((a + 1) to_power n) - ((a - 1) to_power n) > ((a + b) to_power n) - ((a - b) to_power n) & ((a + b) to_power n) - ((a - b) to_power n) > (2 * b) to_power n )