m n k : ℕ+
⊢ Coprime k n → gcd (k * m) n = gcd m n
m n k : ℕ+
⊢ Coprime k n → gcd (m * k) n = gcd m n
rw [mul_comm]
no goals
m n k : ℕ+
⊢ Coprime k n → gcd (k * m) n = gcd m n
apply Coprime.gcd_mul_left_cancel