I need to prove: 256 * (x / 256) <= 256 * x / 256, or more generally forall a b c : N, c > 0 -> a * (b / c) <= a * b / c. This is true since either b is divisible by c and they are equal or it's not and multiplying first can inflate the number and result in greater precision. However, I could not find any theorem in the standard library that proves this, and no automatic tactic I know (auto, intuition, easy, zify and omega) worked. If it helps, I also know that x < 256 * 256, but checking all 65536 cases is not a good proof...
In my specific case I was able to solve it like this:
rewrite (N.mul_comm 256 x).
This switches around the right side to 256 * (x / 256) <= x * 256 / 256.
rewrite (N.div_mul x 256).
This reduced the right side to 256 * (x / 256) <= x.
rewrite (N.mul_div_le x 256).
After this automated tactics are sufficient.