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