Afin de pouvoir démontrer formellement la correction d'algorithmes géométriques en Coq, il est nécessaire de disposer d'outils pour automatiser au moins partiellement les démonstrations en géométrie. Nous étudions cette question dans le cadre simple de la géométrie projective en utilisant une approche combinatoire et la notion de rang d'un ensemble de points. L'outil proposé, implanté en C, procède par saturation du contexte et permet de démontrer automatiquement de nombreux théorèmes emblématiques de la géométrie projective. Afin de s'assurer de la correction de ces démonstrations, l'outil produit une trace sous la forme d'un script de preuve, qui est ensuite vérifié par Coq.