for p being prime Element of NAT
for m, n being non zero Element of NAT st m,n are_coprime & p |^ 2 divides m * n & not p |^ 2 divides m holds
p |^ 2 divides n