proposition: Lemma circumcenter_intersect : forall A B C A' B' C' G, A<>B -> B<>C -> A<>C -> G <> A' -> G <> B' -> G <> 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 G C' A B.
proof: Proof. intros. assert (Cong B G C G). apply (perp_bisect_cong2 G A' B C ). assumption. assert (Cong A G B G). assert (Cong A G C G). apply (perp_bisect_cong2 G B' A C). assumption. CongR. apply perp_col1 with C'; Col. apply perp_right_comm. apply per_perp; auto. apply midpoint_distinct_1 with B; Midpoint. exists B. split; Cong. Qed.
imports: GeoCoq.Highschool.midpoint_thales GeoCoq.Highschool.exercises