Library GeoCoq.Axioms.tarski_axioms

This version of the axioms of Tarski is the one given in Wolfram Schwabhäuser, Wanda Szmielew and Alfred Tarski, Metamathematische Methoden in der Geometrie, Springer-Verlag, Berlin, 1983.
This axioms system is the result of a long history of axiom systems for geometry studied by Tarski, Schwabhäuser, Szmielew and Gupta.

Class Tarski_neutral_dimensionless :=
 Tpoint : Type;
 Bet : Tpoint Tpoint Tpoint Prop;
 Cong : Tpoint Tpoint Tpoint Tpoint Prop;
 cong_pseudo_reflexivity : A B, Cong A B B A;
 cong_inner_transitivity : A B C D E F,
   Cong A B C D Cong A B E F Cong C D E F;
 cong_identity : A B C, Cong A B C C A = B;
 segment_construction : A B C D,
    E, Bet A B E Cong B E C D;
 five_segment : A A' B B' C C' D D',
   Cong A B A' B'
   Cong B C B' C'
   Cong A D A' D'
   Cong B D B' D'
   Bet A B C Bet A' B' C' A B Cong C D C' D';
 between_identity : A B, Bet A B A A = B;
 inner_pasch : A B C P Q,
   Bet A P C Bet B Q C
    X, Bet P X B Bet Q X A;
 PA : Tpoint;
 PB : Tpoint;
 PC : Tpoint;
 lower_dim : ¬ (Bet PA PB PC Bet PB PC PA Bet PC PA PB)

Class Tarski_neutral_dimensionless_with_decidable_point_equality
 `(Tn : Tarski_neutral_dimensionless) :=
 point_equality_decidability : A B : Tpoint, A = B ¬ A = B

Class Tarski_2D
 `(TnEQD : Tarski_neutral_dimensionless_with_decidable_point_equality) :=
 upper_dim : A B C P Q,
   P Q Cong A P A Q Cong B P B Q Cong C P C Q
   (Bet A B C Bet B C A Bet C A B)

Class Tarski_2D_euclidean `(T2D : Tarski_2D) :=
 euclid : A B C D T,
   Bet A D T Bet B D C AD
    X, Y,
   Bet A B X Bet A C Y Bet X T Y