proposition: Lemma is_circumcenter_cases : forall A B C G, 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 -> is_circumcenter G A B C.
proof: Proof. intros. decompose [or] H;clear H; first [apply is_circumcenter_perm in H0|apply is_circumcenter_perm in H1]; spliter; assumption. Qed.
imports: GeoCoq.Highschool.midpoint_thales GeoCoq.Highschool.exercises