Theorem: mod_neg_right (ECTate/Init/Data/Int/Lemmas.lean)

State before:
m k : Int
⊢ m % -k = m % k
Tactic:
simp
State after:
no goals