Theorem: Misc.Nat.sub_mod_eq_zero_of_mod_eq (LeanSAT/Util/Misc.lean)

State before:
m n k : Nat
h : m % k = n % k
⊢ (m - n) % k = 0
Tactic:
rw [← Nat.mod_add_div m k, ← Nat.mod_add_div n k, ← h, Nat.sub_add_eq,
  Nat.add_sub_cancel_left, ← Nat.mul_sub_left_distrib, Nat.mul_mod_right]
State after:
no goals