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