Yes, and it has been done: http://geocoq.github.io/GeoCoq/ http://geocoq.github.io/GeoCoq/ This is actually seriously non-trivial, because Euclid isn't rigorou

Yes, and it has been done: http://geocoq.github.io/GeoCoq/ http://geocoq.github.io/GeoCoq/ This is actually seriously non-trivial, because Euclid isn't rigorous enough for Coq. For example, you need definition of betweenness and Pasch's axiom at the very least.