proposition: Lemma tangentcc__neq: forall A B C D, A<>B -> TangentCC A B C D -> A<>C.
proof: Proof. intros. unfold TangentCC in *. unfold unique in *. ex_and H0 T. intro. subst C. unfold OnCircle in *. assert(Cong A B A D) by (apply cong_transitivity with A T; Cong). assert(T = B). apply(H1 B); Cong. subst T. assert(HH:=symmetric_point_construction B A). ex_and HH B'. unfold Midpoint in *. spliter. assert(B = B'). apply(H1 B'); split; Cong. apply cong_transitivity with A B; Cong. subst B'. treat_equalities; tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Axioms.continuity_axioms