Neron, Pierre. “A Formal Proof of Square Root and Division Elimination in Embedded Programs”. Journal of Formalized Reasoning 6, no. 1 (January 1, 2013): 89–111. Accessed June 5, 2025. https://jfr.unibo.it/article/view/3887.