proposition: Lemma intercc__neq : forall A B C D, InterCC A B C D -> A<>C.
proof: Proof. intros. unfold InterCC in *. ex_and H P. ex_and H0 Q. unfold InterCCAt in *. spliter. unfold OnCircle in *. intro. subst C. apply H. unfold EqC. unfold OnCircle in *. assert(Cong A B A D) by (apply cong_transitivity with A P; Cong). intro. split. intro. apply cong_transitivity with A B; Cong. intro. apply cong_transitivity with A D; Cong. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Axioms.continuity_axioms