Constructive Mathematics and Diaconescu's Theorem in Coq.pdf