How to add a "new" theorem?

[Boutry]

I see that there is a html file that seems to match the page. But there are also some .v. To add an already formalized theorem that belongs to the list, namely #12: The Independence of the Parallel Postulate, should I create a PR with just the added part for the html or also the necessary .v files allowing to verify this?

[jmadiot]

I added some instructions in the README (in particular do not edit the html but the statements.yml file instead).

I'm not sure I understand the situation exactly, but if the statement is already in GeoCoq then only a link to its location is necessary. Otherwise, if there is a single self-contained file, then adding it here is fine. However if the .v files depend on GeoCoq, adding them here would imply extra complexity, dependencies and CI build time, so it might be best to add them somewhere else. Maybe in GeoCoq itself?