proposition: Lemma Euler_line : forall A B C G H O, ~ Col 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. elim (cong_dec A B A C); intro. Name A' the midpoint of B and C. Name B' the midpoint of A and C. Name C' the midpoint of A and B. assert (Perp_bisect A A' B C) by (apply cong_mid_perp_bisect; Cong; intro; treat_equalities; apply H0; Col). assert (Col G A' A) by (apply is_gravity_center_perm in H1; apply is_gravity_center_col with B C; spliter; Col). unfold is_orthocenter in *; spliter. elim (eq_dec_points O G); intro; treat_equalities; Col; elim (eq_dec_points O H); intro; treat_equalities; Col. elim (eq_dec_points O A'); intro; treat_equalities. assert (Col A H O) by (apply cop_perp2__col with B C; Col; Cop; apply perp_bisect_perp; Col). apply is_gravity_center_coplanar in H1. apply col_permutation_1; apply cop_perp2__col with B C. CopR. apply perp_sym; apply perp_col0 with A O; try apply perp_bisect_perp; Col. apply perp_sym; apply perp_col0 with A H; Col. assert (Col A A' H) by (apply cop_perp2__col with B C; Cop; apply perp_bisect_perp; auto). assert (Perp_bisect O A' B C) by (assert_diffs; apply circumcenter_perp with A; auto). assert (Col A' A O) by (apply cop_perp2__col with B C; Perp; Cop). show_distinct A A'. apply H0; Col. ColR. Name A' the symmetric of A wrt O. assert_diffs. assert (Concyclic A B C A'). unfold Concyclic. split. destruct (eq_dec_points A O). treat_equalities; Cop. apply coplanar_perm_12, col_cop__cop with O; Col; Cop. exists O. apply circumcenter_cong in H3. spliter. assert_congs_perm. spliter;repeat (split;finish). assert (T:=concyclic_not_col_or_eq A B C A' H5). decompose [or] T;clear T;try contradiction. - subst. assert (Per A B C). apply midpoint_thales with O;finish. unfold is_circumcenter in *;spliter;finish. apply (Euler_line_special_case A B C G H O);finish. - subst. assert (Per A C B). apply midpoint_thales with O;finish. unfold is_circumcenter in *;spliter. apply cong_transitivity with O B;finish. apply (Euler_line_special_case A C B G H O);finish. apply is_gravity_center_perm_1; assumption. auto with Orthocenter. auto with Circumcenter. - unfold is_circumcenter in *;spliter. treat_equalities. intuition. - spliter. assert_diffs. assert (Per A B A'). apply midpoint_thales with O;finish. unfold is_circumcenter in *;spliter;finish. assert (Perp C H A B) by (unfold is_orthocenter in *;spliter;finish). assert (Perp A' B B A) by (apply per_perp;finish). assert (Par C H A' B). unfold Concyclic in *; spliter. apply is_orthocenter_coplanar in H2. apply l12_9 with A B; try CopR; Perp. assert (Perp B H A C) by (unfold is_orthocenter in *;spliter;finish). assert (Per A C A'). { apply midpoint_thales with O;finish. unfold is_circumcenter in *;spliter;finish. apply cong_transitivity with B O;finish. } assert (Perp A' C C A) by (apply per_perp;finish). assert (Par B H C A'). unfold Concyclic in *; spliter. apply l12_9 with A C; try CopR; Perp. induction (col_dec B H C). * assert (H=B \/ H=C) by (apply (orthocenter_col A B C H);finish). induction H26. + subst H. assert (Midpoint O A C) by (apply (circumcenter_per) with B;finish). assert (Col G O B). apply (is_gravity_center_col A C B G O). apply is_gravity_center_perm in H1;intuition idtac. assumption. Col. + subst H;assert_diffs; intuition. * assert (Parallelogram B H C A') by (apply par_2_plg;finish). assert (T:exists I : Tpoint, Midpoint I B C /\ Midpoint I H A') by (apply plg_mid;finish). destruct T as [I [HI1 HI2]]. elim (per_dec B A C); intro. apply Euler_line_special_case with B A C; try apply is_gravity_center_cases; auto; try apply is_orthocenter_cases; auto; try apply is_circumcenter_cases; auto. assert (is_gravity_center G A H A'). { apply gravity_center_change_triangle with B C I;finish. show_distinct A' H; treat_equalities. apply plg_par in H26; spliter; assert_diffs; Col. intro. Name A'' the midpoint of B and C. show_distinct A'' O; treat_equalities. apply H27; apply perp_per_1; assert_diffs; Perp. assert (Perp_bisect O A'' B C) by (apply circumcenter_perp with A; Col). elim (eq_dec_points A A''); intro; treat_equalities. eauto using perp_bisect_cong_2 with cong. assert (Perp_bisect A'' A B C). apply perp_mid_perp_bisect; Col. apply perp_sym; apply perp_col0 with O A''; Col; try (apply perp_bisect_perp; assumption); assert_cols; try ColR. eauto using perp_bisect_cong_2 with cong. } assert (is_gravity_center G A A' H) by (apply is_gravity_center_cases;auto). perm_apply (is_gravity_center_col A A' H 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