proposition: Lemma interccat__neq : forall A B C D P Q, InterCCAt A B C D P Q -> A <> C.
proof: Proof. intros. apply intercc__neq with B D. unfold InterCC. exists P; exists Q;auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Axioms.continuity_axioms