Function vstd::arithmetic::mul::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