proposition: Lemma col3 : forall X Y A B C, X <> Y -> Col X Y A -> Col X Y B -> Col X Y C -> Col A B C.
proof: Proof. intros. assert (Col X A B) by (apply col_transitivity_1 with Y; assumption). induction(eq_dec_points C X). subst X; apply col_permutation_1; assumption. apply col_permutation_1. apply col_transitivity_1 with X; try assumption. apply col_permutation_2. apply col_transitivity_1 with Y; assumption. apply col_permutation_2. apply col_transitivity_1 with Y; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le