proposition: Lemma concyclic_perm_19 : forall A B C D, Concyclic A B C D -> Concyclic D A C B.
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