proposition: Lemma homothetique_orthocentre : 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 -> O = homothetie (- / 2) G H.
proof: Proof. intros. apply vecteur_homothetie. cut (vec O H = mult_PP 3 (vec O G)); intros. 2: apply droite_Euler_fort with (1 := H0); auto. replace (vec G H) with (add_PP (mult_PP (-1) (vec O G)) (vec O H)); [ idtac | Ringvec ]. rewrite H4. cut (2 <> 0); intros; auto with real. replace (mult_PP (- / 2) (add_PP (mult_PP (-1) (vec O G)) (mult_PP 3 (vec O G)))) with (mult_PP (/ 2) (mult_PP 2 (vec G O))); [ idtac | Ringvec ]. replace (mult_PP (/ 2) (mult_PP 2 (vec G O))) with (mult_PP (/ 2 * 2) (vec G O)); [ idtac | Ringvec ]. replace (/ 2 * 2) with 1; auto with real. Ringvec. Qed.