let a be positive Nat; :: thesis: for n, m being Nat st n >= m holds
a |^ n >= a |^ m
let n, m be Nat; :: 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