proposition: Lemma onc2__oreq : forall A B C D P Q, InterCCAt A B C D P Q -> forall Z, OnCircle Z A B -> OnCircle Z C D -> Z=P \/ Z=Q.
proof: Proof. intros. assert(HCop := all_coplanar A C P Q). assert(HCop1 := all_coplanar A C P Z). apply(cop_onc2__oreq A B C D); assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Axioms.continuity_axioms