have MULTIPLE: n = 0 + (n / modulus) * modulus := by {
  rewrite [<- MODZERO];
  rewrite [Nat.mul_comm];
  simp [Nat.mod_add_div];
}
n modulus : ℕ
MODZERO : n % modulus = 0
⊢ n / modulus * modulus = n
n modulus : ℕ
MODZERO : n % modulus = 0
MULTIPLE : n = 0 + n / modulus * modulus
⊢ n / modulus * modulus = n