The purpose of this webpage is to provide the Coq formalization discussed in:
Reynald Affeldt. On Construction of a Library of Formally Verified Low-level Arithmetic Functions, 9(2):59-77, 2013. NASA/Springer. pdf.
Formalization: simu_begcd.tar.gz (as of 2017/01/06)
BEGCDINSTALL in the root directory.