let a, b be Integer; :: thesis: ( a ^2 divides b ^2 implies a divides b )
assume A1: a ^2 divides b ^2 ; :: thesis: a divides b
A2: ( |.a.| = a or |.a.| = - a ) by COMPLEX1:71;
A3: ( |.b.| = b or |.b.| = - b ) by COMPLEX1:71;
( a ^2 = |.a.| ^2 & b ^2 = |.b.| ^2 ) by COMPLEX1:75;
then |.a.| divides |.b.| by A1, PYTHTRIP:6;
hence a divides b by A2, A3, INT_2:10; :: thesis: verum