m n a b c✝ d c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD c * n]
m n a b c✝ d c : ℕ
h : a ≡ b [MOD n]
⊢ a * c ≡ b * c [MOD n * c]
rw [mul_comm a, mul_comm b, mul_comm n]
no goals
m n a b c✝ d c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD c * n]
exact h.mul_left' c