theorem LME: :: COMPLEX3:71

for a, b being positive Real
for n being Real holds
( (a + b) to_power n > (a to_power n) + (b to_power n) iff ( n is heavy & n is positive ) )