proposition: Lemma midpoint_thales_reci_circum : forall A B C O: Tpoint, Per A C B -> Midpoint O A B -> is_circumcenter O A B C.
proof: Proof. intros. assert (T:= midpoint_thales_reci A B C O H H0). spliter. split;finish. Qed.
imports: GeoCoq.Highschool.midpoint_thales GeoCoq.Highschool.exercises