Function vstd::arithmetic::mul::lemma_mul_is_mul_pos

x >= 0,

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).