Function vstd::arithmetic::mul::lemma_mul_is_distributive_sub

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

Expand description

ensures

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

Proof that multiplication distributes over subtraction, specifically that x * (y - z) == x * y - x * z

Function vstd::arithmetic::mul::lemma_mul_is_distributive_subCopy item path