vstd::arithmetic::mul

Function lemma_mul_inequality_converse

Source 
pub broadcast proof fn lemma_mul_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, that x <= y.