vstd::arithmetic::mul

Function lemma_mul_strictly_increases

Source 
pub broadcast proof fn lemma_mul_strictly_increases(x: int, y: int)
Expand description
requires
1 < x,
0 < y,
ensures
y < #[trigger] (x * y),

Proof that since x > 1 and y > 0, y < x * y.