proposition: Lemma concyclic_aux : forall A B C D, Concyclic A B C D -> exists O P, OnCircle A O P /\ OnCircle B O P /\ OnCircle C O P /\ OnCircle D O P /\ Coplanar A B C O.
proof: Proof. intros A B C D [HCop [O1 [P1]]]; spliter. destruct (col_dec A B C). exists O1, P1; repeat split; Cop. destruct (l11_62_existence A B C O1) as [O []]. exists O, A. assert (HCong := onc2__cong O1 P1). repeat split; [Circle|apply cong2_per2__cong with O1 O1; finish..|assumption]. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel