Rieu-Helft, R. (2019). A Why3 proof of GMP algorithms. Journal of Formalized Reasoning, 12(1), 53–97. https://doi.org/10.6092/issn.1972-5787/9730