. Axiom-pasch, (triple A B J) = 2 /\ rk (triple C D J) = 2. Axiom three_points : forall A B, exists C, rk (triple A B C

M. Bezem and D. Hendriks, On the Mechanization of the Proof of Hessenberg???s Theorem in Coherent Logic, Journal of Automated Reasoning, vol.19, issue.1, pp.61-85, 2008.
DOI : 10.1007/s10817-007-9086-x

J. Brandt and K. Schneider, Using Three-Valued Logic to Specify and Verify Algorithms of Computational Geometry, ICFEM, pp.405-420, 2005.
DOI : 10.1007/11576280_28

C. Cerroni, Non-Desarguian geometries and the foundations of geometry from David Hilbert to Ruth Moufang, Historia Mathematica, vol.31, issue.3, pp.320-336, 2004.
DOI : 10.1016/S0315-0860(03)00049-1

H. S. Coxeter, Projective Geometry, 1987.

C. Dehlinger, J. Dufourd, and P. Schreck, Higher-Order Intuitionistic Formalization and Proofs in Hilbert???s Elementary Geometry, ADG'00, volume 2061 of LNAI, pp.306-324, 2000.
DOI : 10.1007/3-540-45410-1_17

L. Dorst, D. Fontijne, and S. Mann, Geometric algebra for computer science, ACM SIGACT News, vol.39, issue.4, 2007.
DOI : 10.1145/1466390.1466396

J. Filliâtre and P. Letouzey, Functors for Proofs and Programs, LNCS, vol.2986, pp.370-384, 2004.
DOI : 10.1007/978-3-540-24725-8_26

B. Grégoire, L. Pottier, and L. Théry, Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving. Submitted for publication in LNAI as the post-proceedings of ADG'08, 2009.

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

C. M. Hoffmann and R. Joan-arinyo, Handbook of Computer Aided Geometric Design, chapter Parametric Modeling, pp.519-541, 2002.

P. Jani?i´jani?i´c, J. Narboux, and P. Quaresma, The area method : a recapitulation, 2009.

C. Jermann, G. Trombettoni, B. Neveu, and P. Mathis, DECOMPOSITION OF GEOMETRIC CONSTRAINT SYSTEMS: A SURVEY, International Journal of Computational Geometry & Applications, vol.16, issue.05n06, pp.5-6379, 2006.
DOI : 10.1142/S0218195906002105
URL : https://hal.archives-ouvertes.fr/hal-00481267

E. Kusak, Desargues theorem in projective 3-space, J. of Formalized Mathematics, vol.2, 1990.

N. Magaud, J. Narboux, and P. Schreck, Formalizing Projective Plane Geometry in Coq. Submitted for publication in LNAI as the postproceedings of ADG'08, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00305998

L. Meikle and J. Fleuriot, Formalizing Hilbert???s Grundlagen in Isabelle/Isar, TPHOLs'03, pp.319-334, 2003.
DOI : 10.1007/10930755_21

D. Michelucci, S. Foufou, L. Lamarque, and P. Schreck, Geometric constraints solving, Proceedings of the 2006 ACM symposium on Solid and physical modeling , SPM '06, pp.185-196, 2006.
DOI : 10.1145/1128888.1128915
URL : https://hal.archives-ouvertes.fr/hal-01246071

D. Michelucci and P. Schreck, INCIDENCE CONSTRAINTS: A COMBINATORIAL APPROACH, International Journal of Computational Geometry & Applications, vol.16, issue.05n06, pp.5-6443, 2006.
DOI : 10.1142/S0218195906002130

F. R. Moulton, A Simple Non-Desarguesian Plane Geometry. Transactions of the, pp.192-195, 1902.
DOI : 10.1090/s0002-9947-1902-1500595-3

J. Narboux, A Decision Procedure for Geometry in Coq, LNCS, vol.3223, pp.225-240, 2004.
DOI : 10.1007/978-3-540-30142-4_17
URL : https://hal.archives-ouvertes.fr/inria-00001035

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

R. Pouzergues, Les hexamys, 1993.