GeoCoq

GeoCoq: A formalization of geometry in Coq based on Tarski’s axiom system. This library contains a formalization of geometry using the Coq proof assistant. It contains both proofs about the foundations of geometry and high-level proofs in the same style as in high-school.