simp at MULTIPLE
n modulus : ℕ
MODZERO : n % modulus = 0
MULTIPLE : n = 0 + n / modulus * modulus
⊢ n / modulus * modulus = n
n modulus : ℕ
MODZERO : n % modulus = 0
MULTIPLE : n = n / modulus * modulus
⊢ n / modulus * modulus = n