let p be prime Element of NAT ; :: thesis:
let a, b be non zero Element of NAT ; :: thesis:
assume that
A1: a,b are_coprime and
A2: p |^ 2 divides a * b ; :: thesis:
p divides p |^ 2 by NAT_3:3;
then A3: p divides a * b by A2, NAT_D:4;

per cases by A3, NEWTON:80;

suppose p divides a ; :: thesis:

then A4: not p divides b by A1, PYTHTRIP:def 2;
p,b are_coprime

reconsider k = p gcd b as Element of NAT by ORDINAL1:def 12;
assume not p,b are_coprime ; :: thesis:
then A5: k <> 1 by INT_2:def 3;
( k divides p & k divides b ) by NAT_D:def 5;
hence contradiction by A4, A5, INT_2:def 4; :: thesis:

end;

then p * p,b are_coprime by EULER_1:14;
then p |^ 2,b are_coprime by WSIERP_1:1;
hence ( p |^ 2 divides a or p |^ 2 divides b ) by A2, EULER_1:13; :: thesis:

end;

suppose p divides b ; :: thesis:

then A6: not p divides a by A1, PYTHTRIP:def 2;
p,a are_coprime

reconsider k = p gcd a as Element of NAT by ORDINAL1:def 12;
assume not p,a are_coprime ; :: thesis:
then A7: k <> 1 by INT_2:def 3;
( k divides p & k divides a ) by NAT_D:def 5;
hence contradiction by A6, A7, INT_2:def 4; :: thesis:

end;

then p * p,a are_coprime by EULER_1:14;
then p |^ 2,a are_coprime by WSIERP_1:1;
hence ( p |^ 2 divides a or p |^ 2 divides b ) by A2, EULER_1:13; :: thesis:

end;

end;