Function vstd::arithmetic::mul::lemma_mul_strict_inequality_converse

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

Proof that since x * z < y * z and z >= 0, we know x < y