m n a b c✝ d c : ℕ
h : a % n = b % n
⊢ c * a % (c * n) = c * b % (c * n)
m n a b c✝ d c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD c * n]
unfold ModEq at *
no goals
m n a b c✝ d c : ℕ
h : a % n = b % n
⊢ c * a % (c * n) = c * b % (c * n)
rw [mul_mod_mul_left, mul_mod_mul_left, h]