Using something like Geocoq [0] to check the proof would be amazing.

[0] http://geocoq.github.io/GeoCoq/