Function vstd::arithmetic::div_mod::lemma_mul_hoist_inequality

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

Proof that multiplying an integer by a fraction is equivalent to multiplying the fraction’s numerator by the integer. Specifically, x * (y / z) == (x * y) / z.