proposition: Lemma circumcenter_perp_all : forall A B C A' B' C' G, A<>B -> B<>C -> A<>C -> G <> A' -> G <> B' -> G <> C' -> is_circumcenter G A B C -> Midpoint A' B C -> Midpoint B' A C -> Midpoint C' A B -> Perp_bisect G A' B C /\ Perp_bisect G B' A C /\ Perp_bisect G C' A B.
proof: Proof. intros. unfold is_circumcenter in *; spliter. split; [|split]; apply cong_mid_perp_bisect; trivial; CongR. Qed.
imports: GeoCoq.Highschool.midpoint_thales GeoCoq.Highschool.exercises