Function vstd::arithmetic::mul::lemma_mul_inequality
source · pub broadcast proof fn lemma_mul_inequality(x: int, y: int, z: int)Expand description
requires
x <= y,z >= 0,#[trigger] (x * z) <= #[trigger] (y * z),Proof that, since x <= y and z >= 0, x * z <= y * z