let k, m, n be Nat; :: thesis: ( k <= n implies m |^ k divides m |^ n )
assume k <= n ; :: thesis: m |^ k divides m |^ n
then consider t being Nat such that
A1: n = k + t by NAT_1:10;
m |^ n = (m |^ k) * (m |^ t) by A1, NEWTON:8;
hence m |^ k divides m |^ n ; :: thesis: verum