theorem MIN1: :: NEWTON05:9

for a being non zero Nat
for m, n being Nat holds min ((a |^ n),(a |^ m)) = a |^ (min (n,m))