feat(data/int/gcd): another version of Euclid's lemma (#10622)
We already have something described as "Euclid's lemma" in `ring_theory/unique_factorization_domain`, but not this specific statement of the lemma.
This is Theorem 1.5 in Apostol (1976) Introduction to Analytic Number Theory
