Require Export GeoCoq.Tarski_dev.Annexes.midpoint_theorems.
Require Export GeoCoq.Highschool.circumcenter.
Require Export GeoCoq.Highschool.orthocenter.
Require Export GeoCoq.Highschool.midpoint_thales.
Require Export GeoCoq.Highschool.concyclic.
Require Export GeoCoq.Highschool.gravityCenter.

Section Euler_line.

Context `{TE:Tarski_euclidean}.

(**
<applet name="ggbApplet" code="geogebra.GeoGebraApplet" archive="geogebra.jar"
        codebase="http://www.geogebra.org/webstart/4.0/unsigned/"
        width="796" height="466">
        <param name="ggbBase64" value="UEsDBBQACAAIALt4u0QAAAAAAAAAAAAAAAAWAAAAZ2VvZ2VicmFfamF2YXNjcmlwdC5qc0srzUsuyczPU0hPT/LP88zLLNHQVKiuBQBQSwcI1je9uRkAAAAXAAAAUEsDBBQACAAIALt4u0QAAAAAAAAAAAAAAAAMAAAAZ2VvZ2VicmEueG1s3VvbcptIGr7OPEWXLvYqQn0GsnKmnGRm4qpkPLXObm3tTQpBWyJGoAFkS6l5qX2Rfab9uxsQCEuxHNtRksRpoH/68H3/qbvx+OfVPEHXKi/iLD0ZEAcPkErDLIrT6clgWV4OvcHPL38aT1U2VZM8QJdZPg/KkwHXknF0MsBeNPGFr4ZcRRL+CydDf3JJhhPJsO9j5bJADBBaFfGLNPs9mKtiEYTqIpypefAuC4PSdDwry8WL0ejm5sapu3KyfDqaTifOqogGCIaZFieD6uIFNNd56YYZcYoxGf37/Tvb/DBOizJIQzVAegrL+OVPz8Y3cRplN+gmjsrZycDDMI2ZiqczmJPUNyMttABAFios42tVwKutWzPncr4YGLEg1fXP7BVKmukMUBRfx5HKAR+HCuYCBFkeq7SsBEjV0ahuYnwdqxvblr4y3fABKrMsmQS6GfTXX4hiitFzXRBbUCiktFXYPsPMFtQW3BbCynD7Orei3MpwK8PZAF3HRTxJ1MngMkgKgC1OL3OgrLkvynWizHiqB5spk+cwpyL+DMJM42hxhucYP9c/AO5zXgPcmiRp9VrmywM7rbsUHrt7l/RrumR1lxTf0iUVO2Yp94Brx3CXaRLRQha6Mv/MT69HRg/o0d5/XYeSP8kUx6PaUsaVcaBipmUrJks1L7S5MB8JX2s9QQJMQ7qg5AIRHwqXIjAGRATiAm6Jh6QuXcRcqOCIIQ9pOcKQsQ3hwX/cNY1JJKAx/dQFk0QEOuJIMESMSXEEhoSMWYKJUgYSQiABL+nuCdVNMIm4hDvmIQ5j1BbpEhBk8CLcQ/cUMYKYfpm4iEokdXuEa0uXnh46NEmRxEgS3SAYNRi0NWaQ9xDTs5EVXHG6WJYdiMJ5VF+W2aLhAqTBHW08nXVPHUf4bJwEE5VAbLjQTCJ0HSTaIkxHl1laoppEap9N82Axi8PiQpUlvFWgT8F18C4o1epXkC7qvo1smKXFH3lWvs6S5TwtEAqzBDdjzhLSuqbNqOGGtSp4u0K0KmTr2r213wxq0LJQ0H+WF7V4EEVnWmLjGgDJ8zRZv8pVcLXI4u40xiMTZsZqGSZxFAfpv0BZdS8aF1RHHeOt6qjDuVcPJMuji3UBGoxW/1F5Bj6GE4eL1l93gNa2imHpEG/zF8y9CANte1x034HYs95ZZXpW1w1BwUpt5jrNtWG3bs6KV1myeWSm/zpYlMvc5Aswq1xP6jSdJsqoiDFsCMbh1SRbXVjdYLatD+sF3GE7gsnUwI7ANVABA55W5cSWRkYPrZHCRgYbCVwrWxw19cSnRsKUE1saKdBeO7RqqqSeJsF1N3FhM5tBZTa1s9K6r2P7Mo3Ld/VNGYdXm6nqF35fzieq0aBum+Sh2hyPtlRsfKXyVCWVRgOZy2xZWANtKXukwngOt7aigiTQdP0TBmCfRmqaq3rgicnFLGCmFreVtffYNPVrns3P0usPoAtbAxiP6lGOizCPF1rn0ASiwJXaaFUUFwEEkaj9njZBmHqogwXAU2powDiX5SzLTboFPgVKbXmJmkOehUqjXkZDG5hPTdam8UTZ5BO4tSby2foNYVB9q6oZpQySxSzQmV016SRYq7wDg2nvfRZtgwPYmxmAjS8stwulrFrY8cLFApoz1tTxUYB2gVYwAAf0ea3zbx/i7WebstucVU9Vm1jHK9unWzyB8liUvoDXq+8fryFzhGcQw452BY+M2OvvHzHu6GR1rXFiD6NiYTafB2mEUpMK/pEl62mWDjbJSYC1aaKAaI1DAdUwWoyWZV2/gLeIlQmtTAAFhP6J7a3q4xZ6bG81AbadbiAoIUW5gmVYYZYGZRWXzMXbOIqUSU9H+4ltQdlmlghmuBWkilQbaskh1O7Wv0JN9V0zkPALGnj4QA/UwbYmwXq1/UcYvRoKx/WsYvmOi/2WDNuO0XenRv2Z2lcKGzjj+SKJw7hsNCnROn+WlhBGlYkj/eh4pdRCpyXn6Yc8SAu912FlWlH3jjQEx0PDEDu8ywPmhgjXca2BDz1HUs439eSH4WFyRDwwR3ZpqOyBOL609uCCBG3x8D3ZQ9fLv48jGxlvdfN9//7mS268HWXf3CvK6g2KqS0mtvh6ThmswQyJcPEYwfIdML8F4SsL4ZsehNF+CLUSNQhFfQS7K5IddtFddj2EUUBCazNa6bjWCoZEpyDS25hBb+n2MGZwsPZW0J/2oP/lEO395Wi0FyKD9A341PHZ06jvL7s8gDpAfdWxqC9xhF+txzxRaS+4AgKZ8xOrbOPJt/COLN6qh/dvh+jsb0ejs5Az+syVmPnVH2bwF8SRTFZxlAItRPAHVOTzvJxlsI4IkltUugpqQQ/iywNU+vJYVHpo08L1rsTR5u0E02/poPfyUbnpSY+P6QF8TI+FD5sdrnfkj5oN7DDqtdh4pOz9cN9zaYmY9oh4e4jveXs0vkdyhzPie7wB2uyTQNrOPMlb1mCcECyqPLdlPw/pj7TWv4o15Fm+BXrfDc0OUPvZsaj9HdwQdVzS3j14rOXSvWjoe5/4ABriY6Hhi95HONglLRKePBTscj4z63ziHg/nhzif86NxPq4jhU9JQ4J1Ppw7wsMbN1OtQh/V+byP87yn71USdN6D+/RvwSIr/n4I6PUr94H+wfbSW64IckspMfGES13OKOey3rjxIBxwxrkAXijB3iOsoV7HeZhspzjn9Xb5NtpX+3EOszQOGwSv7rc59kBO5l4uIp6q9Nr42wKhFa4+WVtj2z/6XD9ZERM4dB2pHn0mLWrmQZnHK3Ray5/WUqdUE6tDi8CccNcnVAq9X33Kqj5OuWmaSun74PuYpB5zjYQwOiEEh+SYui6HVMGvT/e3nZv+rCK+BDL2kr/3sKQ2E3Mc0lcFfdRBq1T4I6kOTcwFzCS4m1X2D0/o0x+emLJnzvwQbTtgw/gj+bot49tHe/+c03Hdto8hdTT2Oi7JBmPuEN/3hCRSr4yJFI+0DfEtDlSOjJchuAjRcf5us5tPmO8RTl0qpCuEqM9YsE+wzyXFwncfa4PoWzBzp2j9xOzsOHtsjh6H3/XZYzdImM+ttkNEExs2p+r9fev//Xd/ADCf8zQUgrR+H0a1rHCHYOdi15eMShcinS+9L7n6fUkbwf2c4q6n5F+x7AjysJWj1V9SJEl28w91maiVgfeuXNwesF9bHt7WodqE4FZi3IvbrPrUoY7bszpuTz7qkM4bq/tIDg/h7OlCOO4Y91N8/nDfMLF7pA8XIojcGyIIOC1CPb3BxJmPBfueXNJ+WmZHRAtzSDejaj5L8WhnlWdJkXopwDdx+8cJ3NqXHAspO7KpHZbyo+dSR2Qtw21zqZi53VqEwzyPNx6M+nuYYUfGzJ0+AXjbXXpvx+6zQ7a5zo5mbxE71O/tsBvzI6zz+DE+EriobOAgoD/tB3rbrj59052uDdDC8SlYiPR8zPQv4NF6Ne8TiplLuOCehESa1QccGDJr7rrg6KRHiHsXR0eOxJ5G7Y/2za/GVL/Z+fL/UEsHCHiX1BNKCgAAdjoAAFBLAQIUABQACAAIALt4u0TWN725GQAAABcAAAAWAAAAAAAAAAAAAAAAAAAAAABnZW9nZWJyYV9qYXZhc2NyaXB0LmpzUEsBAhQAFAAIAAgAu3i7RHiX1BNKCgAAdjoAAAwAAAAAAAAAAAAAAAAAXQAAAGdlb2dlYnJhLnhtbFBLBQYAAAAAAgACAH4AAADhCgAAAAA=" />
        <param name="image" value="http://www.geogebra.org/webstart/loading.gif" />
        <param name="boxborder" value="false" />
        <param name="centerimage" value="true" />
        <param name="java_arguments" value="-Xmx512m -Djnlp.packEnabled=true" />
        <param name="cache_archive" value="geogebra.jar, geogebra_main.jar, geogebra_gui.jar, geogebra_cas.jar, geogebra_algos.jar, geogebra_export.jar, geogebra_javascript.jar, jlatexmath.jar, jlm_greek.jar, jlm_cyrillic.jar, geogebra_properties.jar" />
        <param name="cache_version" value="4.0.19.0, 4.0.19.0, 4.0.19.0, 4.0.19.0, 4.0.19.0, 4.0.19.0, 4.0.19.0, 4.0.19.0, 4.0.19.0, 4.0.19.0, 4.0.19.0" />
        <param name="showResetIcon" value="false" />
        <param name="showAnimationButton" value="true" />
        <param name="enableRightClick" value="false" />
        <param name="errorDialogsActive" value="true" />
        <param name="enableLabelDrags" value="false" />
        <param name="showMenuBar" value="false" />
        <param name="showToolBar" value="false" />
        <param name="showToolBarHelp" value="false" />
        <param name="showAlgebraInput" value="false" />
        <param name="useBrowserForJS" value="true" />
        <param name="allowRescaling" value="true" />
C'est une appliquette Java créée avec GeoGebra ( www.geogebra.org) - Il semble que Java ne soit pas installé sur votre ordinateur, merci d'aller sur www.java.com
</applet>
*)

Lemma concyclic_not_col_or_eq_aux :
  forall A B C D, Concyclic A B C D -> A = B \/ A = C \/ B = C \/ ~ Col A B C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Concyclic Tn A B C D), or (@eq (@Tpoint Tn) A B) (or (@eq (@Tpoint Tn) A C) (or (@eq (@Tpoint Tn) B C) (not (@Col Tn A B C)))) *)
intros A B C D HC.
(* Goal: or (@eq (@Tpoint Tn) A B) (or (@eq (@Tpoint Tn) A C) (or (@eq (@Tpoint Tn) B C) (not (@Col Tn A B C)))) *)
elim (eq_dec_points A B); intro HAB; Col.
(* Goal: or (@eq (@Tpoint Tn) A B) (or (@eq (@Tpoint Tn) A C) (or (@eq (@Tpoint Tn) B C) (not (@Col Tn A B C)))) *)
elim (eq_dec_points A C); intro HAC; Col.
(* Goal: or (@eq (@Tpoint Tn) A B) (or (@eq (@Tpoint Tn) A C) (or (@eq (@Tpoint Tn) B C) (not (@Col Tn A B C)))) *)
elim (eq_dec_points B C); intro HBC; Col5.
(* Goal: or (@eq (@Tpoint Tn) A B) (or (@eq (@Tpoint Tn) A C) (or (@eq (@Tpoint Tn) B C) (not (@Col Tn A B C)))) *)
right; right; right; intro HCol.
(* Goal: False *)
destruct HC as [HCop [O [HCong1 [HCong2 HCong3]]]].
(* Goal: False *)
assert (H := midpoint_existence A B); destruct H as [M1 HMid1].
(* Goal: False *)
assert (HOM1 : O <> M1).
(* Goal: @is_gravity_center Tn G A H A' *)
(* Goal: @Col Tn G H O *)
  {
(* Goal: not (@eq (@Tpoint Tn) O M2) *)
  intro; treat_equalities.
  assert (H := l7_20 O A C); elim H; clear H; try intro H; Cong;
  try (apply HBC; apply symmetric_point_uniqueness with A O; Col);
  assert_cols; ColR.
  }
(* Goal: False *)
assert (H := midpoint_existence A C); destruct H as [M2 HMid2].
(* Goal: False *)
assert (HOM2 : O <> M2).
(* Goal: @is_gravity_center Tn G A H A' *)
(* Goal: @Col Tn G H O *)
  {
(* Goal: not (@eq (@Tpoint Tn) O M2) *)
  intro; treat_equalities.
  assert (H := l7_20 O A B); elim H; clear H; try intro H; Cong;
  try (apply HBC; apply symmetric_point_uniqueness with A O; Col);
  assert_cols; ColR.
  }
(* Goal: False *)
assert (HM1M2 : M1 <> M2) by (intro; treat_equalities; Col).
assert (HPerp1 : Perp_bisect O M1 A B)
  by (apply cong_cop_perp_bisect; spliter; Cong; Cop).
assert (HPerp2 : Perp_bisect O M2 A C)
  by (apply cong_cop_perp_bisect; spliter; Cong; Cop).
(* Goal: False *)
assert (HOM1M2 : ~ Col O M1 M2).
(* Goal: @is_gravity_center Tn G A H A' *)
(* Goal: @Col Tn G H O *)
  {
  intro HOM1M2; assert (H := l7_20 O A B); elim H; clear H; try intro H; Cong;
  try (apply HOM1; apply l7_17 with A B; Col); assert_diffs; assert_cols; ColR.
  }
(* Goal: False *)
assert (HPar_strict : Par_strict O M1 O M2).
(* Goal: @is_gravity_center Tn G A H A' *)
(* Goal: @Col Tn G H O *)
  {
(* Goal: @Par_strict Tn O M1 O M2 *)
  apply par_not_col_strict with M2; Col.
(* Goal: @Par Tn O M1 O M2 *)
  apply l12_9 with A B; [Cop| |Cop..| |].
(* Goal: @Coplanar Tn A B O M2 *)
(* Goal: @Perp Tn O M1 A B *)
(* Goal: @Perp Tn O M2 A B *)
    apply coplanar_perm_16, col_cop__cop with C; Col; Cop.
(* Goal: @Perp Tn O M1 A B *)
(* Goal: @Perp Tn O M2 A B *)
    apply perp_bisect_perp; Col.
(* Goal: @Perp Tn O M2 A B *)
  apply perp_col0 with A C; Col; perm_apply perp_bisect_perp.

  }
(* Goal: False *)
assert (H := not_par_strict_id O M1 M2); Col.
Qed.

Lemma concyclic_not_col_or_eq :
  forall A B C A', Concyclic A B C A' ->
  A'=C \/ A'=B \/ A=B \/ A=C \/ A=A' \/ (~ Col A B A' /\ ~ Col A C A').
Proof.
(* Goal: forall (A B C A' : @Tpoint Tn) (_ : @Concyclic Tn A B C A'), or (@eq (@Tpoint Tn) A' C) (or (@eq (@Tpoint Tn) A' B) (or (@eq (@Tpoint Tn) A B) (or (@eq (@Tpoint Tn) A C) (or (@eq (@Tpoint Tn) A A') (and (not (@Col Tn A B A')) (not (@Col Tn A C A'))))))) *)
intros A B C A' H.
(* Goal: or (@eq (@Tpoint Tn) A' C) (or (@eq (@Tpoint Tn) A' B) (or (@eq (@Tpoint Tn) A B) (or (@eq (@Tpoint Tn) A C) (or (@eq (@Tpoint Tn) A A') (and (not (@Col Tn A B A')) (not (@Col Tn A C A'))))))) *)
assert (H' := H); apply concyclic_perm_1 in H; apply concyclic_perm_3 in H'.
(* Goal: or (@eq (@Tpoint Tn) A' C) (or (@eq (@Tpoint Tn) A' B) (or (@eq (@Tpoint Tn) A B) (or (@eq (@Tpoint Tn) A C) (or (@eq (@Tpoint Tn) A A') (and (not (@Col Tn A B A')) (not (@Col Tn A C A'))))))) *)
apply concyclic_not_col_or_eq_aux in H; apply concyclic_not_col_or_eq_aux in H'.
(* Goal: or (@eq (@Tpoint Tn) A' C) (or (@eq (@Tpoint Tn) A' B) (or (@eq (@Tpoint Tn) A B) (or (@eq (@Tpoint Tn) A C) (or (@eq (@Tpoint Tn) A A') (and (not (@Col Tn A B A')) (not (@Col Tn A C A'))))))) *)
elim (eq_dec_points A' C); intro; try tauto.
(* Goal: or (@eq (@Tpoint Tn) A' C) (or (@eq (@Tpoint Tn) A' B) (or (@eq (@Tpoint Tn) A B) (or (@eq (@Tpoint Tn) A C) (or (@eq (@Tpoint Tn) A A') (and (not (@Col Tn A B A')) (not (@Col Tn A C A'))))))) *)
elim (eq_dec_points A' B); intro; try tauto.
(* Goal: or (@eq (@Tpoint Tn) A' C) (or (@eq (@Tpoint Tn) A' B) (or (@eq (@Tpoint Tn) A B) (or (@eq (@Tpoint Tn) A C) (or (@eq (@Tpoint Tn) A A') (and (not (@Col Tn A B A')) (not (@Col Tn A C A'))))))) *)
elim (eq_dec_points A B); intro; try tauto.
(* Goal: or (@eq (@Tpoint Tn) A' C) (or (@eq (@Tpoint Tn) A' B) (or (@eq (@Tpoint Tn) A B) (or (@eq (@Tpoint Tn) A C) (or (@eq (@Tpoint Tn) A A') (and (not (@Col Tn A B A')) (not (@Col Tn A C A'))))))) *)
elim (eq_dec_points A C); intro; try tauto.
(* Goal: or (@eq (@Tpoint Tn) A' C) (or (@eq (@Tpoint Tn) A' B) (or (@eq (@Tpoint Tn) A B) (or (@eq (@Tpoint Tn) A C) (or (@eq (@Tpoint Tn) A A') (and (not (@Col Tn A B A')) (not (@Col Tn A C A'))))))) *)
elim (eq_dec_points A A'); intro; try tauto.
(* Goal: or (@eq (@Tpoint Tn) A' C) (or (@eq (@Tpoint Tn) A' B) (or (@eq (@Tpoint Tn) A B) (or (@eq (@Tpoint Tn) A C) (or (@eq (@Tpoint Tn) A A') (and (not (@Col Tn A B A')) (not (@Col Tn A C A'))))))) *)
do 3 (elim H; clear H; intro H; try tauto); Col.
(* Goal: or (@eq (@Tpoint Tn) A' C) (or (@eq (@Tpoint Tn) A' B) (or (@eq (@Tpoint Tn) A B) (or (@eq (@Tpoint Tn) A C) (or (@eq (@Tpoint Tn) A A') (and (not (@Col Tn A B A')) (not (@Col Tn A C A'))))))) *)
do 3 (elim H'; clear H'; intro H'; try tauto); Col.
Qed.

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.
(* Goal: forall (A B C G H O : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @is_gravity_center Tn G A B C) (_ : @is_orthocenter Tn H A B C) (_ : @is_circumcenter Tn O A B C), @Col Tn G H O *)
intros.
(* Goal: @Col Tn G H O *)
assert (H=B).
(* Goal: @eq (@Tpoint Tn) H B *)
(* Goal: @Col Tn G H O *)
  apply orthocenter_per with A C;finish.
(* Goal: @Col Tn G H O *)
subst.
(* Goal: @Col Tn G B O *)
assert (Midpoint O A C).
(* Goal: @Midpoint Tn O A C *)
(* Goal: @Col Tn G B O *)
 apply circumcenter_per with B;finish.
(* Goal: not (@eq (@Tpoint Tn) B C) *)
(* Goal: @Col Tn G B O *)
 unfold is_orthocenter in *;spliter;assert_diffs;finish.
(* Goal: not (@eq (@Tpoint Tn) B C) *)
(* Goal: @Col Tn G B O *)
 unfold is_orthocenter in *;spliter;assert_diffs;finish.
(* Goal: @Col Tn G B O *)
assert (is_gravity_center G A C B).
(* Goal: @is_gravity_center Tn G A C B *)
(* Goal: @Col Tn G B O *)
 apply is_gravity_center_perm in H1;intuition.
(* Goal: @Col Tn G B O *)
perm_apply (is_gravity_center_col A C B G O).
Qed.

Lemma gravity_center_change_triangle:
 forall A B C G I B' C',
 is_gravity_center G A B C ->
 Midpoint I B C ->
 Midpoint I B' C' ->
 ~ Col A B' C' ->
 is_gravity_center G A B' C'.
Proof.
(* Goal: forall (A B C G H O : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @is_gravity_center Tn G A B C) (_ : @is_orthocenter Tn H A B C) (_ : @is_circumcenter Tn O A B C), @Col Tn G H O *)
intros.
(* Goal: @is_gravity_center Tn G A B' C' *)
Name G' the midpoint of A and G.
assert (Midpoint G I G')
  by (apply (is_gravity_center_third A B C G G' I);finish).
(* Goal: @is_gravity_center Tn G A B' C' *)
apply (is_gravity_center_third_reci A B' C' G I G');finish.
Qed.

(* Could be removed. See gravityCenter.v. *)
Hint Resolve
     is_gravity_center_perm_1
     is_gravity_center_perm_2
     is_gravity_center_perm_3
     is_gravity_center_perm_4
     is_gravity_center_perm_5 : gravitycenter.

Hint Resolve
     is_orthocenter_perm_1
     is_orthocenter_perm_2
     is_orthocenter_perm_3
     is_orthocenter_perm_4
     is_orthocenter_perm_5 : Orthocenter.

Hint Resolve
     is_circumcenter_perm_1
     is_circumcenter_perm_2
     is_circumcenter_perm_3
     is_circumcenter_perm_4
     is_circumcenter_perm_5 : Circumcenter.


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.
(* Goal: forall (A B C G H O : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @is_gravity_center Tn G A B C) (_ : @is_orthocenter Tn H A B C) (_ : @is_circumcenter Tn O A B C), @Col Tn G H O *)
intros.
(* Goal: @Col Tn G H O *)
elim (cong_dec A B A C); intro.

(* Goal: @Col Tn G H O *)
(* Goal: @Col Tn G H O *)
Name A' the midpoint of B and C.
(* Goal: @Col Tn G H O *)
(* Goal: @Col Tn G H O *)
Name B' the midpoint of A and C.
(* Goal: @Col Tn G H O *)
(* Goal: @Col Tn G H O *)
Name C' the midpoint of A and B.

assert (Perp_bisect A A' B C)
  by (apply cong_cop_perp_bisect; assert_diffs; Cong; Cop; 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).

(* Goal: @Col Tn G H O *)
(* Goal: @Col Tn G H O *)
unfold is_orthocenter in *; spliter.

elim (eq_dec_points O G); intro; treat_equalities; Col;
(* Goal: @Col Tn G B O *)
elim (eq_dec_points O H); intro; treat_equalities; Col.

(* Goal: not (@eq (@Tpoint Tn) O M2) *)
elim (eq_dec_points O A'); intro; treat_equalities.

(* Goal: @Col Tn G H O *)
(* Goal: @Col Tn G H O *)
(* Goal: @Col Tn G H O *)
assert (Col A H O) by (apply cop_perp2__col with B C; Col; Cop; apply perp_bisect_perp; Col).
(* Goal: @Col Tn G H O *)
(* Goal: @Col Tn G H O *)
(* Goal: @Col Tn G H O *)
apply col_permutation_1; apply cop_perp2__col with B C.

(* Goal: @Coplanar Tn B C G H *)
(* Goal: @Perp Tn O G B C *)
(* Goal: @Perp Tn O H B C *)
(* Goal: @Col Tn G H O *)
(* Goal: @Col Tn G H O *)
apply coplanar_trans_1 with A; Cop.
(* Goal: @Perp Tn O M1 A B *)
(* Goal: @Perp Tn O M2 A B *)
apply perp_sym; apply perp_col0 with A O; try apply perp_bisect_perp; Col.
(* Goal: @Perp Tn O H B C *)
(* Goal: @Col Tn G H O *)
(* Goal: @Col Tn G H O *)
apply perp_sym; apply perp_col0 with A H; Col.

(* Goal: @Col Tn G H O *)
(* Goal: @Col Tn G H O *)
assert (Col A A' H) by (apply cop_perp2__col with B C; Cop; apply perp_bisect_perp; auto).
(* Goal: @Col Tn G H O *)
(* Goal: @Col Tn G H O *)
assert (Perp_bisect O A' B C) by (apply circumcenter_perp with A; assert_diffs; Col).
assert (Col A' A O)
  by (apply cop_perp2__col with B C; Cop; apply perp_left_comm; apply perp_bisect_perp; auto).
(* Goal: @Col Tn G H O *)
(* Goal: @Col Tn G H O *)
show_distinct A A'; assert_cols; Col; ColR.

(* Goal: @Col Tn G H O *)
Name A' the symmetric of A wrt O.

(* Goal: @Col Tn G H O *)
assert_diffs.

(* Goal: @Col Tn G H O *)
assert (Concyclic A B C A').
(* Goal: @Concyclic Tn A B C A' *)
(* Goal: @Col Tn G H O *)
 unfold Concyclic.
(* Goal: and (@Coplanar Tn A B C A') (@ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O C) (@Cong Tn O A O A')))) *)
(* Goal: @Col Tn G H O *)
 split.
(* Goal: @Coplanar Tn A B C A' *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O C) (@Cong Tn O A O A'))) *)
(* Goal: @Col Tn G H O *)
 destruct (eq_dec_points A O).
(* Goal: @Coplanar Tn A B C A' *)
(* Goal: @Coplanar Tn A B C A' *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O C) (@Cong Tn O A O A'))) *)
(* Goal: @Col Tn G H O *)
  treat_equalities; Cop.
(* Goal: @Coplanar Tn A B C A' *)
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O C) (@Cong Tn O A O A'))) *)
(* Goal: @Col Tn G H O *)
 apply coplanar_perm_12, col_cop__cop with O; Col; Cop.
(* Goal: @ex (@Tpoint Tn) (fun O : @Tpoint Tn => and (@Cong Tn O A O B) (and (@Cong Tn O A O C) (@Cong Tn O A O A'))) *)
(* Goal: @Col Tn G H O *)
 exists O.
(* Goal: and (@Cong Tn O A O B) (and (@Cong Tn O A O C) (@Cong Tn O A O A')) *)
(* Goal: @Col Tn G H O *)
 apply circumcenter_cong in H3.
(* Goal: @Col Tn G H O *)
 spliter.
(* Goal: and (@Cong Tn O A O B) (and (@Cong Tn O A O C) (@Cong Tn O A O A')) *)
(* Goal: @Col Tn G H O *)
 assert_congs_perm.
(* Goal: and (@Cong Tn O A O B) (and (@Cong Tn O A O C) (@Cong Tn O A O A')) *)
(* Goal: @Col Tn G H O *)
 spliter;repeat (split;finish).

(* Goal: @Col Tn G H O *)
assert (T:=concyclic_not_col_or_eq A B C A' H5).
(* Goal: @Col Tn G H O *)
decompose [or] T;clear T;try contradiction.
(* Goal: @Col Tn G H O *)
 - subst.
(* Goal: @Col Tn G H O *)
   assert (Per A B C).
(* Goal: @Per Tn A C A' *)
    apply midpoint_thales with O;finish.
(* Goal: @Cong Tn O A O C *)
    unfold is_circumcenter in *;spliter;finish.
(* Goal: @Col Tn G H O *)
   apply (Euler_line_special_case A B C G H O);finish.
(* Goal: @Col Tn G H O *)
 - subst.
(* Goal: @Col Tn G H O *)
   assert (Per A C B).
(* Goal: @Per Tn A C A' *)
    apply midpoint_thales with O;finish.
(* Goal: @Col Tn G H O *)
    unfold is_circumcenter in *;spliter.
(* Goal: @Cong Tn O A O C *)
(* Goal: @Col Tn G H O *)
    apply cong_transitivity with O B;finish.

(* Goal: @Col Tn G H O *)
   apply (Euler_line_special_case A C B G H O);finish.
(* For 8.5  bug *)
(* Goal: @is_gravity_center Tn G A C B *)
(* Goal: @is_orthocenter Tn H A C B *)
(* Goal: @is_circumcenter Tn O A C B *)
   try (apply is_gravity_center_perm_1; assumption). 
(* Goal: @is_orthocenter Tn H A C B *)
(* Goal: @is_circumcenter Tn O A C B *)
   auto with Orthocenter.
(* Goal: @is_circumcenter Tn O A C B *)
   auto with Circumcenter.

(* Goal: @Col Tn G H O *)
 - unfold is_circumcenter in *;spliter.
(* Goal: @Col Tn G H O *)
   treat_equalities.
(* Goal: @Col Tn G H C *)
   intuition.
(* Goal: @Col Tn G H O *)
 - spliter.

(* Goal: @Col Tn G H O *)
assert_diffs.

(* Goal: @Col Tn G H O *)
assert (Per A B A').
(* Goal: @Per Tn A C A' *)
 apply midpoint_thales with O;finish.
(* Goal: @Cong Tn O A O C *)
 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).

(* Goal: @Col Tn G H O *)
assert (Par C H A' B).
(* Goal: @Col Tn G H O *)
 unfold Concyclic in *; spliter.
(* Goal: @Par Tn C H A' B *)
(* Goal: @Col Tn G H O *)
 apply l12_9 with A B; [Cop|Cop| |Cop|Perp..].
(* Goal: @Coplanar Tn A B H A' *)
(* Goal: @Col Tn G H O *)
 apply coplanar_trans_1 with C; Col; Cop.

assert (Perp B H A C)
 by (unfold is_orthocenter in *;spliter;finish).

(* Goal: @Col Tn G H O *)
assert (Per A C A').
(* Goal: @is_gravity_center Tn G A H A' *)
(* Goal: @Col Tn G H O *)
 {
(* Goal: @Per Tn A C A' *)
 apply midpoint_thales with O;finish.
(* Goal: @Cong Tn O A O C *)
 unfold is_circumcenter in *;spliter;finish.
(* Goal: @Cong Tn O A O C *)
 apply cong_transitivity with B O;finish.
 }

(* Goal: @Col Tn G H O *)
assert (Perp A' C C A) by (apply per_perp;finish).

(* Goal: @Col Tn G H O *)
assert (Par B H C A').
(* Goal: @Col Tn G H O *)
 unfold Concyclic in *; spliter.
(* Goal: @Par Tn B H C A' *)
(* Goal: @Col Tn G H O *)
 apply l12_9 with A C; [Cop..| |Perp|Perp].
(* Goal: @Coplanar Tn A C H A' *)
(* Goal: @Col Tn G H O *)
 apply coplanar_trans_1 with B; Col; Cop.

(* Goal: @Col Tn G H O *)
induction (col_dec B H C).
 * assert (H=B \/ H=C) by (apply (orthocenter_col A B C H);finish).
(* Goal: @Col Tn G H O *)
   induction H26.
   + subst H.
(* Goal: @Col Tn G B O *)
     assert (Midpoint O A C) by (apply (circumcenter_per) with B;finish).
(* Goal: @Col Tn G B O *)
     assert (Col G O B).
(* Goal: @Col Tn G O B *)
(* Goal: @Col Tn G B O *)
        apply (is_gravity_center_col A C B G O).
(* Goal: @is_gravity_center Tn G A C B *)
(* Goal: @Midpoint Tn O A C *)
(* Goal: @Col Tn G B O *)
        apply is_gravity_center_perm in H1;intuition idtac.
(* Goal: @Midpoint Tn O A C *)
(* Goal: @Col Tn G B O *)
        assumption.
(* Goal: @Col Tn G B O *)
     Col.
(* Goal: @Col Tn G B O *)
   (*  perm_apply (is_gravity_center_col A C B G O). bug in 8.5 *) 
(* Goal: @Col Tn G H C *)
   + 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).

(* Goal: @Col Tn G H O *)
   destruct T as [I [HI1 HI2]].

(* Goal: @Col Tn G H O *)
   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.

(* Goal: @Col Tn G H O *)
   assert (is_gravity_center G A H A').
(* Goal: @is_gravity_center Tn G A H A' *)
(* Goal: @Col Tn G H O *)
     {
(* Goal: @is_gravity_center Tn G A H A' *)
     apply gravity_center_change_triangle with B C I;finish.
(* Goal: @Col Tn G H O *)
     show_distinct A' H; treat_equalities.
(* Goal: @Col Tn G B O *)
     apply plg_par in H26; spliter; assert_diffs; Col.
(* Goal: False *)
(* Goal: not (@Col Tn A H A') *)
     apply H25; apply par_id_5; Par.
(* Goal: not (@Col Tn A H A') *)
     intro.
(* Goal: False *)
     Name A'' the midpoint of B and C.
(* Goal: @Col Tn G H O *)
     show_distinct A'' O; treat_equalities.
(* Goal: False *)
(* Goal: False *)
     apply H27; apply perp_per_1; assert_diffs; Perp.
(* Goal: False *)
     assert (Perp_bisect O A'' B C) by (apply circumcenter_perp with A; Col).
(* Goal: not (@eq (@Tpoint Tn) O M2) *)
     elim (eq_dec_points A A''); intro; treat_equalities.
(* Goal: False *)
     eauto using perp_bisect_cong_2 with cong.
(* Goal: False *)
     assert (Perp_bisect A'' A B C).
(* Goal: @Col Tn G B O *)
     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.
(* Goal: False *)
     eauto using perp_bisect_cong_2 with cong.
     }

   assert (is_gravity_center G A A' H)
     by (apply is_gravity_center_cases;auto).

(* Goal: @Col Tn G H O *)
   perm_apply (is_gravity_center_col A A' H G O).
Qed.

End Euler_line.
