Wenda Li, Lawrence C. Paulson: A modular, efficient formalisation of real algebraic numbers. CPP 2016: 66-75