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.