vstd::arithmetic::mul

Function lemma_mul_basics

Source 
pub proof fn lemma_mul_basics(x: int)
Expand description
ensures
0 * x == 0,
x * 0 == 0,
x * 1 == x,
1 * x == x,