a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd (a * b) m
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd (b * a) m
rw [mul_comm]
no goals
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd (a * b) m
apply Coprime.factor_eq_gcd_left cop am bn