Neron, Pierre. “A Formal Proof of Square Root and Division Elimination in Embedded Programs”. Journal of Formalized Reasoning, vol. 6, no. 1, Jan. 2013, pp. 89-111, doi:10.6092/issn.1972-5787/3887.