Function vstd::arithmetic::mul::lemma_mul_left_inequality

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

Proof that multiplying the positive integer x by respectively y and z maintains the order of y and z. Specifically, y <= z ==> x * y <= x * z and y < z ==> x * y < x * z.