Complete the definition of computer division for alt-ergo

The driver for alt-ergo gave only a partial definition of computer division using euclidean division. The first commit shows a completed version. However it is very easy to make a mistake. So the second commit adds the possibility in a driver to force the use of a theory, and we add a theory ComputerOfEuclideanDivision which define computer division using euclidean division. The last commit prove the lemmas using coq.