Neron, P. A Formal Proof of Square Root and Division Elimination in Embedded Programs. JFR 2013, 6, 89-111.