proposition: Lemma symetrique_milieu_milieu : forall A B C A' B' C' O G H I J : PO, triangle A B C -> A' = milieu B C -> B' = milieu A C -> C' = milieu A B -> G = centre_gravite A B C -> circonscrit O A B C -> H = orthocentre A B C -> I = milieu O H -> J = milieu A H -> J = symetrie I A'.
proof: Proof. unfold symetrie in |- *; intros. Comments Image "file://C:/Documents and Settings/Frédérique Guilhot/.pcoq/figures/f1043312519.gif". elim existence_homothetique with (k := -1) (I := I) (A := A'); intros L H13. rewrite <- H13. apply vecteur_nul_conf. Comments Image "file://C:/Documents and Settings/Frédérique Guilhot/.pcoq/figures/f1043312668.gif". cut (vec H L = vec H J); intros. replace (vec J L) with (add_PP (vec H L) (mult_PP (-1) (vec H J))); [ idtac | Ringvec ]. rewrite <- H9; Ringvec. rewrite (homothetie_bipoint (k:=-1) (I:=I) (A:=O) (B:=A') (A':=H) (B':=L)); auto with geo. rewrite (homothetie_bipoint (k:=- / 2) (I:=G) (A:=H) (B:=A) (A':=O) (B':=A')); auto. cut (2 <> 0); intros; auto with real. replace (mult_PP (-1) (mult_PP (- / 2) (vec H A))) with (mult_PP (-1 * - / 2) (vec H A)); [ idtac | Ringvec ]. replace (-1 * - / 2) with (/ 2); [ idtac | ring ]. rewrite (milieu_vecteur2 (A:=H) (B:=A) (M:=J)); auto with geo. apply (homothetique_orthocentre (A:=A) (B:=B) (C:=C) (O:=O) (G:=G) (H:=H)); auto. apply centre_gravite_homothetie with (1 := H1); auto. Qed.