let a, b be non weightless Integer; :: thesis: ( a,b are_coprime implies ( not a divides b & not b divides a ) )
assume A1: a,b are_coprime ; :: thesis: ( not a divides b & not b divides a )
|.a.| in NAT by INT_1:3;
then reconsider x = |.a.| as non trivial Nat ;
|.b.| in NAT by INT_1:3;
then reconsider y = |.b.| as non trivial Nat ;
x,y are_coprime by A1, INT_2:34;
then ( not x divides y & not y divides x ) by NEWTON03:44;
hence ( not a divides b & not b divides a ) by INT_2:16; :: thesis: verum