proposition: Lemma col_transitivity_1 : forall P Q A B, P<>Q -> Col P Q A -> Col P Q B -> Col P A B.
proof: Proof. intros. induction (eq_dec_points A P). subst; unfold Col; Between. assert (T:=l6_16_1 P Q A B). apply col_permutation_1; apply T; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le