plan
motivations
interface graphique
PCoq
outil de construction
GeoView
géométrie enseignée au lycée
le système formel
les fonctionnalités de
Coq
utilisées
développement en
Coq
théorème de géométrie dans l'espace
l'inversion géométrique
difficultés rencontrées
conclusion
JFLA 2004 F. GUILHOT