proposition: Lemma concyclic_trans : forall A B C D E, ~ Col A B C -> Concyclic A B C D -> Concyclic A B C E -> Concyclic A B D E.
proof: Proof. intros. split. unfold Concyclic in *; spliter; CopR. apply concyclic_aux in H0. apply concyclic_aux in H1. decompose [ex and] H0;clear H0. decompose [ex and] H1;clear H1. exists x. repeat split;Cong. assert (x=x0). assert_diffs. apply is_circumcenter_uniqueness with A B C;try assumption. repeat split; [CongR..|Cop]. repeat split; [CongR..|Cop]. subst. Cong. Qed.
imports: GeoCoq.Highschool.circumcenter