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