m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 ≡ 0 [ZMOD n]
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ a + -a ≡ b + -b [ZMOD n]
simp_rw [← sub_eq_add_neg, sub_self]
no goals
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 ≡ 0 [ZMOD n]
rfl