proposition: Lemma colx : forall A B C X Y, A <> B -> Col X Y A -> Col X Y B -> Col A B C -> Col X Y C.
proof: Proof. intros. destruct (eq_dec_points X Y). subst; Col. apply (col3 A B); auto; apply col_permutation_1. apply col_transitivity_1 with Y; Col. apply (col_transitivity_2 X); Col. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le