Function vstd::arithmetic::div_mod::lemma_div_is_ordered

source · 
pub broadcast proof fn lemma_div_is_ordered(x: int, y: int, z: int)
Expand description
requires
x <= y,
0 < z,
ensures
#[trigger] (x / z) <= #[trigger] (y / z),

Proof that numerical order is preserved when dividing two seperate integers by a common positive divisor. Specifically, given that z > 0 and x <= y, we know x / z <= y / z.