proposition: Lemma circumcenter_cong : forall G A B C, is_circumcenter G A B C -> Cong A G B G /\ Cong B G C G /\ Cong C G A G.
proof: Proof. unfold is_circumcenter. intros. intuition eCong. Qed.
imports: GeoCoq.Highschool.midpoint_thales GeoCoq.Highschool.exercises