Function vstd::arithmetic::mul::lemma_mul_increases

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

Proof that since x and y are both positive, their product is greater than or equal to y