• Formalization of Chapter 16 of SST (this completes the formalization of part one of the book in 2D!) :
  definition of coordinates and characterization of Cong and Bet using coordinates.
• Reorganization of files into directories
• Creation of a ./configure
• Characterization of Midpoint and Col using coordinates.
• Proof of the equivalence between upper-dimension axiom and the fact that all points are coplanar.
• Proof of the pseudo-transitivity and permutation properties of the generalized con-cyclic predicate.
• Definition of the sum of angles and related proofs.
• Proofs about the parallel postulate: assuming a weak geometric version of Archimedes axiom,
  the fact that the sum of angles of a triangle is two rights implies Playfair's postulate.
• Proofs of the decidability of Chapter 11 predicates, assuming points equality decidability.