Function vstd::arithmetic::mul::lemma_mul_is_mul_recursive
source · pub broadcast proof fn lemma_mul_is_mul_recursive(x: int, y: int)Expand description
ensures
#[trigger] (x * y) == mul_recursive(x, y),Proof that multiplication using * is equivalent to
multiplication using a recursive definition. Specifically,
x * y is equivalent in that way.