proposition: Lemma homothetie_mediatrice_hauteur : forall A B C I G J H : PO, triangle A B C -> I <> J -> I = milieu B C :>PO -> mediatrice B C J -> G = centre_gravite A B C :>PO -> H = homothetie (-2) G J :>PO -> orthogonal (vec A H) (vec B C).
proof: Proof. intros. deroule_triangle A B C. cut (-2 <> 0); intros. cut (A = homothetie (-2) G I); intros. cut (A <> H); intros. cut (paralleles (droite I J) (droite A H)); intros. apply paralleles_orthogonal with (3 := H13); auto. apply mediatrice_orthogonale_segment; auto. apply milieu_mediatrice; auto. apply paralleles_sym; auto. apply homothetie_droite with (3 := H11) (4 := H5); auto. apply image_homothetie_distincts with (3 := H11) (4 := H5); auto. replace (-2) with (/ - / 2). apply homothetie_inverse; auto with real. apply centre_gravite_homothetie with (2 := H4); auto. rewrite <- Rinv_opp; auto with real. discrR. Qed.