proposition: Lemma concyclic_perm_17 : forall A B C D, Concyclic A B C D -> Concyclic C D B A.
proof: Proof. intros A B C D H. destruct H as [H1 [X H2]]. split; [Cop|spliter; exists X; repeat split; CongR..]. Qed.
imports: GeoCoq.Highschool.circumcenter