A à pgcd implique A[X] à pgcd

On montre quelques propriétés générales du pgcd avec des preuves par équivalences, puis on arrive au lemme de Gauss qui permet de débloquer la situation comme dans le cas factoriel.