Assia Mahboubi: Programming and certifying a CAD algorithm in the Coq system. Mathematics, Algorithms, Proofs 2005