proposition: Lemma is_circumcenter_perm : forall A B C G, is_circumcenter G A B C -> is_circumcenter G A B C /\ is_circumcenter G A C B /\ is_circumcenter G B A C /\ is_circumcenter G B C A /\ is_circumcenter G C A B /\ is_circumcenter G C B A.
proof: Proof. unfold is_circumcenter. intros. spliter. repeat split;eauto using cong_transitivity with cong;Cop. Qed.
imports: GeoCoq.Highschool.midpoint_thales GeoCoq.Highschool.exercises