let a, b be non trivial Nat; :: thesis: ( a,b are_coprime implies ( not a divides b & not b divides a ) )
assume a,b are_coprime ; :: thesis: ( not a divides b & not b divides a )
then ( 1 = a gcd (b mod a) & 1 = b gcd (a mod b) ) by NAT_D:28;
then A3: ( not b mod a = 0 & not a mod b = 0 ) by Def0;
( a = ((a div b) * b) + (a mod b) & b = ((b div a) * a) + (b mod a) ) by NAT_D:2;
then ( not a = (a div b) * b & not b = (b div a) * a ) by A3;
hence ( not a divides b & not b divides a ) by NAT_D:3; :: thesis: verum