proposition: Theorem droite_Euler : 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 -> alignes O G H.
proof: Proof. intros. apply colineaire_alignes with 3; auto. apply droite_Euler_fort with (1 := H0); auto. Qed.