proposition: Lemma TangentCC_Col : forall A B C D X, TangentCC A B C D -> OnCircle X A B -> OnCircle X C D -> Col X A C.
proof: Proof. intros. unfold TangentCC in *. induction(eq_dec_points A C). subst C. Col. assert(HS:=ex_sym1 A C X H2). ex_and HS Y. ex_and H4 M. assert(Cong X A Y A). apply(is_image_col_cong A C X Y A H2 H6); Col. assert(Cong X C Y C). apply(is_image_col_cong A C X Y C H2 H6); Col. destruct H. unfold unique in H. assert(x =X). apply H. split; auto. subst x. assert(OnCircle Y A B). unfold OnCircle in *. apply cong_transitivity with A X; Cong. assert(OnCircle Y C D). unfold OnCircle in *. apply cong_transitivity with C X; Cong. assert(X = Y). apply H. split; auto. subst Y. unfold Reflect in H6. induction H6. spliter. unfold ReflectL in *. spliter. ex_and H11 Z. assert(Z = X). apply l7_3; auto. subst Z. Col. spliter. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Axioms.continuity_axioms