Rieu-Helft, Raphael. 2019. “A Why3 Proof of GMP Algorithms”. Journal of Formalized Reasoning 12 (1):53-97. https://doi.org/10.6092/issn.1972-5787/9730.