Function vstd::arithmetic::mul::lemma_mul_ordering

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

Proof that, since the product of the two integers x and y is nonnegative, that product is greater than or equal to each of x and y