vstd::arithmetic::mul

Function lemma_mul_upper_bound

Source 
pub broadcast proof fn lemma_mul_upper_bound(x: int, xbound: int, y: int, ybound: int)
Expand description
requires
x <= xbound,
y <= ybound,
0 <= x,
0 <= y,
ensures
#[trigger] (x * y) <= #[trigger] (xbound * ybound),

Proof that since x is bounded above by xbound and y is bounded above by ybound, the product of x and y is bounded above by the product of the bounds.