theorem :: NEWTON05:14

for a being Nat
for b, n being non zero Nat holds (a mod b) |^ n >= (a |^ n) mod b