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.