proposition: Lemma circumcenter_per : forall A B C O, A<>B -> B<>C -> Per A B C -> is_circumcenter O A B C -> Midpoint O A C.
proof: Proof. intros. Name O' the midpoint of A and C. assert (T:= midpoint_thales_reci_circum A C B O' H1 H4). assert (O=O'). apply is_circumcenter_uniqueness with A B C;finish. intro. treat_equalities. apply l8_8 in H1. intuition. auto using is_circumcenter_perm_1. subst;auto. Qed.
imports: GeoCoq.Highschool.midpoint_thales GeoCoq.Highschool.exercises