Function vstd::arithmetic::mul::lemma_mul_basics_2
source · pub broadcast proof fn lemma_mul_basics_2(x: int)Expand description
ensures
#[trigger] (x * 0) == 0,Proof of basic properties of multiplication by x, specifically
what happens when multiplying by 0 or 1