The following while loop implements a way to multiply two numbers that was developed by the ancient Egyptians: Algorithm : (Note that the indentations describe the code blocks that apply to the scope of the while and if statements.) [Pre-condition : A and B are positive integers, x = A , y = B, and product = 0.] while (y != 0) r := (y mod 2) if (r= 0) then do x:= 2 *x y:=y div 2 end do if (r=1) then do product=product+x y=y 1 end do end while [Post-condition: product = A * B] Prove the correctness of this loop with respect to its pre and post-conditions by using the loop invariant I(n) : (x * y) + product = (A * B).