Function vstd::arithmetic::mul::lemma_mul_is_distributive_add

source · 
pub broadcast proof fn lemma_mul_is_distributive_add(x: int, y: int, z: int)
Expand description
ensures
#[trigger] (x * (y + z)) == x * y + x * z,

Proof that multiplication distributes over addition, specifically that x * (y + z) == x * y + x * z