no goals
m✝ n a✝ b✝ c✝ d a b c m : ℕ
hc : c ≠ 0
⊢ a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m]
simp [modEq_iff_dvd, ← sub_mul, mul_dvd_mul_iff_right (by simp [hc] : (c : ℤ) ≠ 0)]
no goals
m✝ n a✝ b✝ c✝ d a b c m : ℕ
hc : c ≠ 0
⊢ ↑c ≠ 0
simp [hc]