Function vstd::arithmetic::mul::lemma_mul_strict_upper_bound
source · pub broadcast proof fn lemma_mul_strict_upper_bound(x: int, xbound: int, y: int, ybound: int)Expand description
requires
x < xbound,y < ybound,0 < x,0 < y,#[trigger] (x * y) <= #[trigger] ((xbound - 1) * (ybound - 1)),Proof that when x has an exclusive upper bound xbound and y
has an exclusive upper bound ybound, that the product of x and
y is bounded above by the product of the predecessors of their
upper bounds. In other words, x * y <= (xbound - 1) * (ybound - 1).