let m, n be Nat; :: thesis: ( m is square-free & n divides m implies n is square-free )
assume that
A1: m is square-free and
A2: n divides m ; :: thesis: n is square-free
ex x being Nat st m = n * x by A2, NAT_D:def 3;
hence n is square-free by A1, Th25; :: thesis: verum