proposition: Lemma is_circumcenter_perm_1 : forall A B C G, is_circumcenter G A B C -> is_circumcenter G A C B.
proof: Proof. intros. apply is_circumcenter_perm in H;intuition. Qed.
imports: GeoCoq.Highschool.midpoint_thales GeoCoq.Highschool.exercises