proposition: Lemma circumcenter_perp : forall A B C A' G, A<>B -> B<>C -> A<>C -> G <> A' -> is_circumcenter G A B C -> Midpoint A' B C -> Perp_bisect G A' B C.
proof: Proof. intros. apply cong_cop_perp_bisect; try assumption; unfold Midpoint, is_circumcenter in *; spliter; Cong; Cop. Qed.
imports: GeoCoq.Highschool.midpoint_thales GeoCoq.Highschool.exercises