let a be natural positive number ; :: thesis: for n, m being natural number st n >= m holds
a |^ n >= a |^ m
let n, m be natural number ; :: thesis: ( n >= m implies a |^ n >= a |^ m )
assume n >= m ; :: thesis: a |^ n >= a |^ m
then a |^ m divides a |^ n by NEWTON:89;
hence a |^ n >= a |^ m by INT_2:27; :: thesis: verum