Reduction mod m

Stream: maths

[Patrick Stevens]

For the life of me I can't find lemma reduce_mod (m n : nat) : (n / m) * m + (n % m) = n := by sorry, and it absolutely has to be somewhere. library_search gives me nothing; no variant on "div_mul" or "div_mod" or "division_alg" that I've tried has given me anything. Can someone point me to it?

[Bhavik Mehta]

There's lemma mod_add_div (m k : ℕ) : m % k + k * (m / k) = m := in core

[Patrick Massot]

It's annoying to have a hard time finding this. Should we have variants? I guess there are four possibilities, excluding the eq.symm variations

[Patrick Stevens]

Excluding the symm variations seems correct; I would hardly expect a lemma to go from simple to more complex

[Patrick Massot]

Well, the real world statement would clearly be in the other direction.

[Patrick Massot]

But library_search will see through that.