tentative update of https://gitlab.inria.fr/bertot/cadcoq references: Root Isolation for one-variable polynomials https://wiki.portal.chalmers.se/cse/uploads/ForMath/rootisol Theorem of three circles in Coq https://arxiv.org/abs/1306.0783