theorem Integers.ideal_span_pair_eq_span_gcd (a b : ℤ) : Ideal.span {a, b} = Ideal.span {↑(a.gcd b)}