Мне нужно доказать: 256 * (x / 256) <= 256 * x / 256 или, в более общем смысле, forall a b c : N, c > 0 -> a * (b / c) <= a * b / c.Это верно, так как либо b делится на c, и они равны, либо нет, и умножение в первую очередь может увеличить число и привести к большей точности.Однако я не смог найти ни одной теоремы в стандартной библиотеке, которая бы это доказывала, и ни одна из известных мне автоматических тактик (auto, intuition, easy, zify и omega) не сработала.Если это поможет, я также знаю, что x < 256 * 256, но проверка всех 65536 случаев не является хорошим доказательством ...