let k be Nat; :: thesis: ( k > 1 implies not k * k divides k )
assume A1: k > 1 ; :: thesis: not k * k divides k
assume A2: k * k divides k ; :: thesis: contradiction
k divides k * k ;
then k * k = k by A2, NAT_D:5;
then k * (k - 1) = 0 ;
then ( k = 0 or k - 1 = 0 ) ;
hence contradiction by A1; :: thesis: verum