let a, b be Integer; :: thesis: for m, n being Nat st a |^ n divides b & not a |^ m divides b holds
m > n
let m, n be Nat; :: thesis: ( a |^ n divides b & not a |^ m divides b implies m > n )
assume ( a |^ n divides b & not a |^ m divides b ) ; :: thesis: m > n
then not a |^ m divides a |^ n by INT_2:9;
hence m > n by NEWTON89; :: thesis: verum