Rieu-Helft, Raphael. “A Why3 Proof of GMP Algorithms”. Journal of Formalized Reasoning 12, no. 1 (January 1, 2019): 53–97. Accessed April 11, 2025. https://jfr.unibo.it/article/view/9730.