for m, p being Nat holds
( not p is prime or m,p are_coprime or m gcd p = p )