# Hilbert's axioms of classical geometry
This is a Rocq implementation of 
"Geometry: Euclid and Beyond" by Robin Hartshorne
(Japanese version).

### attention
: "Definition foo := ..." != "Definition foo : ...", the latter needs a proof.

: Law of excluded middle is not used. If a parameter (terms without any definition)
```distinct_point``` 
is replaced with 
```equal_point```,
you may not be able to prove equality of points without law of ex. Of course, now you cannot prove distinction of points without law of ex. Equality semms to be used more frequently when stating conclusions of theorems, so distinction of points is now given as a parameter.