proposition: Lemma circle_circle_cop : forall A B C D I P, OnCircle I A B -> OnCircle I C D -> exists Z, OnCircle Z A B /\ OnCircle Z C D /\ Coplanar A C P Z.
proof: Proof. intros A B C D I P HI1 HI2. destruct (col_dec A C P). exists I; repeat split; trivial. exists P; left; split; Col. destruct (col_dec A C I). exists I; repeat split; trivial. exists I; left; split; Col. destruct (circle_circle_os A B C D I P) as [Z [HZ1 [HZ2 HOS]]]; trivial. exists Z; repeat split; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel