# Claim: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.