proposition: Lemma concyclic_aux : forall A B C D, Concyclic A B C D -> exists O, Cong O A O B /\ Cong O A O C /\ Cong O A O D /\ Coplanar A B C O.
proof: Proof. intros A B C D [HCop [O1]]; spliter. destruct (col_dec A B C). exists O1; repeat split; Cop. destruct (l11_62_existence A B C O1) as [O []]. exists O. repeat split; try apply cong2_per2__cong with O1 O1; finish. Qed.
imports: GeoCoq.Highschool.circumcenter