Function vstd::arithmetic::mul::lemma_mul_is_associative

pub broadcast proof fn lemma_mul_is_associative(x: int, y: int, z: int)

Expand description

ensures

x * (y * z) == (x * y) * z,

Proof that multiplication is associative, specifically that x * (y * z) == (x * y) * z.