Function vstd::arithmetic::mul::lemma_mul_is_distributive_sub_other_way

source ·

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

Expand description

ensures

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

Proof that multiplication distributes over subtraction when the subtraction happens in the multiplicand (i.e., in the left-hand argument to *). Specifically, (y - z) * x == y * x - z * x.