proposition: Theorem droite_Euler_fort : forall A B C O G H : PO, triangle A B C -> G = centre_gravite A B C -> circonscrit O A B C -> H = orthocentre A B C -> vec O H = mult_PP 3 (vec O G).
proof: Proof. intros. rewrite <- (centre_gravite_prop_vecteur (A:=A) (B:=B) (C:=C) (G:=G) O); auto. elim existence_representant_som_vecteur with (A := O) (B := B) (C := O) (D := C); intros E H4; try clear existence_representant_som_vecteur; rewrite <- H4. elim existence_representant_som_vecteur with (A := O) (B := A) (C := O) (D := E); intros M H5; try clear existence_representant_som_vecteur; rewrite <- H5. cut (M = H); intros. rewrite <- H6; auto. rewrite H3. apply vec_OAplusOBplusOC_orthocentre with O; auto. rewrite <- H4; auto. Qed.