vstd::arithmetic::mul

Function lemma_mul_by_zero_is_zero

Source 
pub broadcast proof fn lemma_mul_by_zero_is_zero(x: int)
Expand description
ensures
x * 0 == 0 && 0 * x == 0,

Proof that any integer multiplied by 0 results in a product of 0.