Inductiveformalproof Let A and B be two positive integers, and Q and R the quotient and the remainder of the division of A by B. Q and R are defined by the property:

A = Q * B + R. Consider the following program annotated by the assertions Al, A2, A3:

-- Al: A>O and B>O R:= Ai Q:= Oi while R>=B loop

-- A2: A = Q * B + Rand R>=B R:= R - Bi Q:= Q + 1i end looPi

-- A3: A = Q * B + Rand R A3 after the program execution. Is this demonstration a proof that the program is correct?