( (1 / a) to_power (- b) is heavy & (1 / a) to_power (- b) is positive ) ;
then a to_power (- (- b)) is heavy by POWER:32;
hence a to_power b is heavy ; :: thesis: verum