let p, n be Nat; :: thesis: ( p is prime & p,n are_coprime implies not p divides n )
assume that
A1: p is prime and
A2: p,n are_coprime ; :: thesis: not p divides n
assume p divides n ; :: thesis: contradiction
then n gcd p = p by NEWTON:49;
then n gcd p > 1 by A1, INT_2:def 4;
hence contradiction by A2, INT_2:def 3; :: thesis: verum