Div and mod

pre: 0 < A and A <= B

A =
B =

post: r = A mod B and q = A div B
= { logic rewrite }
post: A = q * B + r and 0 <= r < B
r = 0
q = 1

no div or mod operators were used.
program requires A+B-1 loops worse-case.



check source for proof.

Show meh!