Function vstd::arithmetic::mul::lemma_mul_nonnegative

source · 
pub broadcast proof fn lemma_mul_nonnegative(x: int, y: int)
Expand description
requires
0 <= x,
0 <= y,
ensures
0 <= #[trigger] (x * y),

Proof that since x and y are non-negative, their product is non-negative