Theorem: Int.Int.neg_emod_eq_zero_iff (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p k : ℤ
⊢ -p % k = 0 ↔ p % k = 0
Tactic:
simp [← Int.dvd_iff_emod_eq_zero]
State after:
no goals