P. Neron, “A Formal Proof of Square Root and Division Elimination in Embedded Programs”, JFR, vol. 6, no. 1, pp. 89–111, Jan. 2013.