Simplified the algorithm for Smith on PIDs.

I removed some equality proofs that were mixed in the function
improve_pivot_rec. The flip side is some technicality in the proofs, due to
dependent types, casts and induction.