A case study in formalizing projective geometry in Coq: Desargues theorem

Nicolas Magaud, Julien Narboux, Pascal Schreck. A case study in formalizing projective geometry in Coq: Desargues theorem. Comput. Geom., 45(8):406-424, 2012. [doi]

Abstract

Abstract is missing.