case inl
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ c * a ≡ c * b [ZMOD c * n]

case inr.inl
m n a b d : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 * a ≡ 0 * b [ZMOD 0 * n]

case inr.inr
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
hc : 0 < c
⊢ c * a ≡ c * b [ZMOD c * n]
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD c * n]
obtain hc | rfl | hc := lt_trichotomy c 0
case inl
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ -c * a ≡ -c * b [ZMOD -c * n]
case inl
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ c * a ≡ c * b [ZMOD c * n]
rw [← neg_modEq_neg, ← modEq_neg, ← neg_mul, ← neg_mul, ← neg_mul]
no goals
case inl
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ -c * a ≡ -c * b [ZMOD -c * n]
simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq]
no goals
case inr.inl
m n a b d : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 * a ≡ 0 * b [ZMOD 0 * n]
simp
no goals
case inr.inr
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
hc : 0 < c
⊢ c * a ≡ c * b [ZMOD c * n]
simp only [ModEq, mul_emod_mul_of_pos _ _ hc, h.eq]