let a, b, m be Nat; :: thesis: ( b > 0 implies a < a + (b |^ m) )
assume b > 0 ; :: thesis: a < a + (b |^ m)
then b |^ m > 0 by PREPOWER:6;
hence a < a + (b |^ m) by NAT_1:16; :: thesis: verum