proposition: Lemma homothetique_centre_circonscrit : forall A B C O G H I : PO, triangle A B C -> G = centre_gravite A B C -> circonscrit O A B C -> H = orthocentre A B C -> I = milieu O H -> I = homothetie (- / 2) G O.
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. cut (2 <> 0); intros; auto with real. apply mult_PP_regulier with 2; auto. replace (mult_PP 2 (vec G I)) with (add_PP (vec G O) (vec G H)). replace (vec G H) with (add_PP (vec G O) (vec O H)); [ idtac | Ringvec ]. rewrite H5. replace (mult_PP 2 (mult_PP (- / 2) (vec G O))) with (mult_PP (2 * / 2) (vec O G)); [ idtac | Ringvec ]. replace (2 * / 2) with 1; auto with real. Ringvec. rewrite (prop_vecteur_milieu (B:=O) (C:=H) (A':=I) G); auto. Qed.