Function lemma_mul_is_mul_posCopy item path

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