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 April 26, 2024. https://jfr.unibo.it/article/view/3887.