*Proof*.
We leave to the reader the proof of the uniqueness of the
quotient and the remainder of

w.r.t. to

.
So we focus now on the complexity result
Consider an iteration of the

**for** loop
where

holds at the begining of the loop.
Observe that

and

have the same leading coefficient.
Since

, computing the reductum of

requires

operations.
Then subtracting the reductum of

to that of

requires again

operations.
Hence each iteration of the

**for** loop requires at most

operations in

,
since we need also to count

for the computation of

.
The number of

**for** loops is

.
Therefore Algorithm

1
requires

.