According to Wikipedia "Coprime integers", see https://en.wikipedia.org/wiki/Coprime_integers (16-Aug-2020) "[...] two integers a and b are said to be relatively prime, mutually prime, or coprime [...] if the only positive integer (factor) that divides both of them is 1. Consequently, any prime number that divides one does not divide the other. This is equivalent to their greatest common divisor (gcd) being 1.". In the following, we use this equivalent characterization to say that and are coprime (or relatively prime) if . The equivalence of the definitions is shown by coprmgcdb. The negation, i.e. two integers are not coprime, can be expressed either by , see ncoprmgcdne1b, or equivalently by , see ncoprmgcdgt1b.
A proof of Euclid's lemma based on coprimality is provided in coprmdvds (see euclemma for a version of Euclid's lemma for primes).