Library GeoCoq.Axioms.beeson_s_axioms

Class intuitionistic_Tarski_neutral_dimensionless := {
 ITpoint : Type;
 IBet : ITpoint → ITpoint → ITpoint → Prop;
 ICong : ITpoint → ITpoint → ITpoint → ITpoint → Prop;
 Cong_stability : ∀ A B C D, ¬ ¬ ICong A B C D → ICong A B C D;
 Bet_stability : ∀ A B C, ¬ ¬ IBet A B C → IBet A B C;
 IT A B C := ¬ (A≠B ∧ B≠C ∧ ¬ IBet A B C);
 ICol A B C := ¬ (~ IT C A B ∧ ¬ IT A C B ∧ ¬ IT A B C);
 Icong_identity : ∀ A B C, ICong A B C C → A = B;
 Icong_inner_transitivity : ∀ A B C D E F,
   ICong A B C D → ICong A B E F → ICong C D E F;
 Icong_pseudo_reflexivity : ∀ A B, ICong A B B A;
 Isegment_construction : ∀ A B C D,
    A≠B → ∃ E, IT A B E ∧ ICong B E C D;
 Ifive_segment : ∀ A A' B B' C C' D D',
    ICong A B A' B' →
    ICong B C B' C' →
    ICong A D A' D' →
    ICong B D B' D' →
    IT A B C → IT A' B' C' → A ≠ B → ICong C D C' D';
 Ibetween_identity : ∀ A B, ¬ IBet A B A;
 Ibetween_symmetry : ∀ A B C, IBet A B C → IBet C B A;
 Ibetween_inner_transitivity : ∀ A B C D, IBet A B D → IBet B C D → IBet A B C;
 Iinner_pasch : ∀ A B C P Q,
   IBet A P C → IBet B Q C → ¬ ICol A B C →
   ∃ x, IBet P x B ∧ IBet Q x A;
 PA : ITpoint;
 PB : ITpoint;
 PC : ITpoint;
 Ilower_dim : ¬ IT PC PA PB ∧ ¬ IT PA PC PB ∧ ¬ IT PA PB PC
}.