Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

P. Boutry, J. Narboux, P. Schreck, and G. Braun, Using Small Scale Automation to Improve Both Accessibility and Readability of Formal Proofs in Geometry, Automated Deduction in Geometry 2014, pp.1-19, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00989781

G. Braun and J. Narboux, From Tarski to Hilbert, Lecture Notes in Computer Science, vol.7993, pp.89-109, 2012.
DOI : 10.1007/978-3-642-40672-0_7

URL : https://hal.archives-ouvertes.fr/hal-00727117

D. Delahaye, M. Jaume, and V. Prevosto, Coq, un outil pour l'enseignement. Une exp??rience avec les ??tudiants du DESS D??veloppement de logiciels s??rs, Techniques et sciences informatiques, vol.24, issue.9, pp.1139-1160, 2005.
DOI : 10.3166/tsi.24.1139-1160

URL : https://hal.archives-ouvertes.fr/hal-01125076

F. Guilhot, Formalisation en Coq et visualisation d'un cours de g??om??trie pour le lyc??e, Techniques et sciences informatiques, vol.24, issue.9, pp.1113-1138, 2005.
DOI : 10.3166/tsi.24.1113-1138

M. Jaume and T. Laurent, Teaching Formal Methods and Discrete Mathematics, Proceedings 1st Workshop on Formal Integrated Development Environment, pp.30-43, 2014.
DOI : 10.4204/EPTCS.149.4

URL : https://hal.archives-ouvertes.fr/hal-01203024

C. Lelay, Coquelicot passe le bac Exposé invité, disponible à https, Journées Francophones des Langages Applicatifs (JFLA), 2014.

J. Narboux, Mechanical Theorem Proving in Tarski???s Geometry, Automated Deduction in Geometry, ADG 2006. Revised Papers, pp.139-156, 2007.
DOI : 10.1007/978-3-540-77356-6_9

W. Schwabhauser, W. Szmielew, and A. Tarski, Metamathematische Methoden in der Geometrie, 1983.
DOI : 10.1007/978-3-642-69418-9

A. Annexes, Axiomatique sur les angles, Parameter Point : Set. Definition Point_equal := @eq Point. Parameter Point_col : Point -> Point -> Point -> Prop