How to prove integer division inequality in Coq

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...