Function vstd::arithmetic::div_mod::lemma_div_by_multiple_is_strongly_ordered

source · 
pub broadcast proof fn lemma_div_by_multiple_is_strongly_ordered(x: int, y: int, m: int, z: int)
Expand description
requires
x < y,
y == m * z,
0 < z,
ensures
x / z < y / z,

Proof that a dividend that is a positive multiple of a divisor will always yield a greater quotient than a smaller dividend. Specifically, x / z < y / z because y == m * z and x < y.