let p, q be Prime; :: thesis: ( p <> q implies p,q are_coprime )
assume A1: p <> q ; :: thesis: p,q are_coprime
p gcd q <> p

proof

assume p gcd q = p ; :: thesis: contradiction
then p divides q by INT_2:def 2;
then ( p = q or p = 1 ) by INT_2:def 4;
hence contradiction by A1, INT_2:def 4; :: thesis: verum

end;

hence p,q are_coprime by NEWTON03:46; :: thesis: verum