Col (A B C : Point) : Prop := Bet A B C \/ Bet B C A \/ Bet C A B
col_permutation_1 : forall A B C, Col A B C → Col B C A
col_permutation_2 : forall A B C, Col A B C → Col C A B
col_permutation_3 : forall A B C, Col A B C → Col C B A
col_permutation_4 : forall A B C, Col A B C → Col B A C
col_permutation_5 : forall A B C, Col A B C → Col B A C
col_trivial_1 : forall A B, Col A A B
col_trivial_2 : forall A B, Col A B B
col_trivial_3 : forall A B, Col A B A
forall A B C A' B' C', Col A B C → Cong_3 A B C A' B' C' → Col A' B' C'
(voir l4_6)
forall A B C A' B',
Col A B C → Cong A B A' B' → exists C', Cong_3 A B C A' B' C'
(voir l4_5)
FSC := fun A B C D A' B' C' D' =>
Col A B C /\ Cong_3 A B C A' B' C' /\ Cong A D A' D' /\ Cong B D B' D'
forall A B C D A' B' C' D',
FSC A B C D A' B' C' D' → A<>B → Cong C D C' D'
(voir five_segments_with_def - l4_2)
forall A B C P Q,
A<>B → Col A B C → Cong A P A Q → Cong B P B Q → Cong C P C Q
forall A B C C', A ≠ B -> Col A B C → Cong A C A C' → Cong B C B C' → C=C'
forall A B C C', forall A B C C', Bet A C B → Cong A C A C' → Cong B C B C' → C = C'