This new release brings mainly:
- some results about Archimedes' postulates contributed by Charly Gries,
- equivalences between about 30 versions of the parallel postulate by Charly Gries and Pierre Boutry,
- a study of the bisector and incenter contributed by Dan Song,
- a justification of the area method axioms contributed by Julien Narboux
Changelog:
- Add compatibility with Coq 8.5.
- Definition of Archimedes' postulate (geometric version).
- Definition of Archimedes' postulate for angles.
- Archimedes' postulate implies Aristotle's postulate.
- Legendre's theorems.
- Szmielew's theorem about parallel postulates: every proposition which is true in Euclidean geometry and not in Hyperbolic geometry is equivalent to the parallel postulate.
- Predicate TS (Two Sides) cleared of a redundant condition.
- Definition of the interior bisector and related properties.
- Proof of the existence of the incenter of a triangle.
- Proof of the existence of an equilateral triangle build on a given base without any continuity axiom (in any Pythagorean field).
- Justification of the axioms of the area method.