let m, p be Nat; :: thesis: ( not p is prime or m,p are_coprime or m gcd p = p )
A1: m gcd p divides p by NAT_D:def 5;
assume p is prime ; :: thesis: ( m,p are_coprime or m gcd p = p )
then ( m gcd p = 1 or m gcd p = p ) by A1, INT_2:def 4;
hence ( m,p are_coprime or m gcd p = p ) by INT_2:def 3; :: thesis: verum