theorem SqCon1: :: MOEBIUS2:54

for n, k being non zero Nat st k <> 1 & k ^2 divides n holds
n is square-containing