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.