# Proof:Euclidean division algorithm

For all and all , there exists numbers and such that

Here and are the quotient and remainder of over :

Definition: Quotient
We say is a quotient of over if for some with . We write (note that quot is a well defined function).
Definition: Remainder
We say is a remainder of over if for some and . We write (note that rem is a well defined function).

Note that all this is a theorem, it is called the "Euclidean division algorithm" because its proof contains an algorithm.

Proof:
We prove this by weak induction on . Let be the statement "for all , there exists satisfying (1) and (2) above." We will show and assuming .

Base case: We want to show P(0). Let . Then and since .

Inductive step: Assume ; we want to show . By , we know that there exists numbers and such that . We want to show that there exists numbers and such that .

Since , we know that either or . In the former case, we can let and . Then (and clearly ).

In the latter case, we can let and . Then . Again it is clear that .

In either case, we have shown that there exist and satisfying (1) and (2), as required.