Prove the correctness of the following loop:

count = n;

fact = 1;

while count <> 0 do

fact = fact * count;

count = count - 1;

end

{fact = n!}