proposition: Lemma exists_circumcenter : forall A B C, ~ Col A B C -> exists G, is_circumcenter G A B C.
proof: Proof. intros. assert (triangle_circumscription_principle). apply (inter_dec_plus_par_perp_perp_imply_triangle_circumscription). unfold decidability_of_intersection; apply inter_dec. unfold perpendicular_transversal_postulate. intros; apply cop_par_perp__perp with A0 B0; auto. unfold triangle_circumscription_principle in *. destruct (H0 A B C H) as [G HG]. exists G. unfold is_circumcenter. spliter. repeat split;Cop;CongR. Qed.
imports: GeoCoq.Highschool.midpoint_thales GeoCoq.Highschool.exercises