feat(RingTheory/Coprime/Lemmas): Add Int.isCoprime_gcdA/B (leanprover-community#32369)

Adds Int.isCoprime_gcdA and  Int.isCoprime_gcdB

Author: metakunt

Mathlib/RingTheory/Coprime/Lemmas.lean

@@ -62,6 +62,14 @@ theorem Nat.Coprime.cast {R : Type*} [CommRing R] {a b : ℕ} (h : Nat.Coprime a
 theorem Rat.isCoprime_num_den (x : ℚ) : IsCoprime x.num x.den :=
   x.reduced.cast.of_isCoprime_of_dvd_left Int.dvd_natAbs_self
 
+theorem Int.isCoprime_gcdA {x y : ℤ} (h : IsCoprime x y) : IsCoprime (x.gcdA y) y := by
+  use x, x.gcdB y
+  rwa [mul_comm _ y, ← Int.gcd_eq_gcd_ab, Nat.cast_eq_one, ← Int.isCoprime_iff_gcd_eq_one]
+
+theorem Int.isCoprime_gcdB {x y : ℤ} (h : IsCoprime x y) : IsCoprime (x.gcdB y) x := by
+  use y, x.gcdA y
+  rwa [add_comm, mul_comm , ← Int.gcd_eq_gcd_ab, Nat.cast_eq_one, ← Int.isCoprime_iff_gcd_eq_one]
+
 theorem ne_zero_or_ne_zero_of_nat_coprime {A : Type u} [CommRing A] [Nontrivial A] {a b : ℕ}
     (h : Nat.Coprime a b) : (a : A) ≠ 0 ∨ (b : A) ≠ 0 :=
   IsCoprime.ne_zero_or_ne_zero (R := A) <| by