proposition: Lemma concyclic_1123 : forall A B C, ~ Col A B C -> Concyclic A A B C.
proof: Proof. intros A B C HABC. unfold Concyclic. split. apply coplanar_trivial. destruct (exists_circumcenter A B C HABC) as [G HG]. exists G. apply circumcenter_cong in HG;spliter;repeat split;Cong. Qed.
imports: GeoCoq.Highschool.circumcenter