proposition: Lemma interccat__ncol : forall A B C D P Q, InterCCAt A B C D P Q -> ~ Col A C P.
proof: Proof. intros. intro. assert (HH := H). unfold InterCCAt in HH. spliter. apply H2. apply (l4_18 A C). apply interccat__neq in H. auto. assumption. apply cong_transitivity with A B; Cong. apply cong_transitivity with C D; Cong. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Axioms.continuity_axioms