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