Laurent Fuchs, Laurent Théry: A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry. Automated Deduction in Geometry 2010: 51-67