proposition: Lemma is_circumcenter_coplanar : forall A B C G, is_circumcenter G A B C -> Coplanar G A B C.
proof: Proof. unfold is_circumcenter; intros; spliter; assumption. Qed.
imports: GeoCoq.Highschool.midpoint_thales GeoCoq.Highschool.exercises