Nous présentons dans ce rapport une bibliothèque de géométrie en Coq dédiée-l'enseignement au lycée. L'accent est porté sur l'utilisation de l'interface graphique Pcoq et sur l'outil de construction GeoView qui permettent de présenter des énoncés et des figures proches de ceux utilisés au lycée. L'axiomatique choisie pour la formalisation n'utilise pas la méthode analytique. Nous présentons quelques exemples significatifs de preuves puis abordons les difficultés rencontrées dans ce travail.