some simplifications to coherent in old development
fix a proof in cprufer