proposition: Lemma Euler_line_special_case : forall A B C G H O, Per A B C -> is_gravity_center G A B C -> is_orthocenter H A B C -> is_circumcenter O A B C -> Col G H O.
proof: Proof. intros. assert (H=B). apply orthocenter_per with A C;finish. subst. assert (Midpoint O A C). apply circumcenter_per with B;finish. unfold is_orthocenter in *;spliter;assert_diffs;finish. unfold is_orthocenter in *;spliter;assert_diffs;finish. assert (is_gravity_center G A C B). apply is_gravity_center_perm in H1;intuition. perm_apply (is_gravity_center_col A C B G O). Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.circumcenter GeoCoq.Highschool.orthocenter GeoCoq.Highschool.midpoint_thales GeoCoq.Highschool.concyclic GeoCoq.Highschool.gravityCenter