Let div₂(n) = floor(n/2) (i.e., the largest integer that is less than or equal to n/2). Alternatively, think of it as the function that performs division by 2 on a binary number by shifting right one digit. Prove that the following program correctly multiplies two natural numbers. Clearly state the loop invariant that you are using.

mult(n, m: natural numbers) =

result = 0.

While m != 0 do

If odd(m) then result = result + n.

n = 2n.

m = div₂(m).