Function vstd::arithmetic::mul::lemma_mul_basics_4

source · 
pub broadcast proof fn lemma_mul_basics_4(x: int)
Expand description
ensures
#[trigger] (1 * x) == x,

Proof of basic properties of multiplication by x, specifically what happens when multiplying by 0 or 1