Function vstd::arithmetic::mul::lemma_mul_is_distributive_add_other_way

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

Expand description

ensures

#[trigger] ((y + z) * x) == y * x + z * x,

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