Proof-oriented version of Smith on PIDs.

It is the same algorithm as the one used on Euclidean rings. Only the
termination proof is more involved (and some more dependent types), which
makes it less well-suited for computations.