Function vstd::arithmetic::mul::lemma_mul_is_mul_pos

source · 
pub proof fn lemma_mul_is_mul_pos(x: int, y: int)
Expand description
requires
x >= 0,
ensures
x * y == mul_pos(x, y),

Proof that multiplying two positive integers with * results in the same product as would be achieved by recursive addition. Specifically, x * y == mul_pos(x, y).