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