proposition: Lemma triangle_triangle_milieux : forall A B C A' B' C' : PO, triangle A B C -> A' = milieu B C :>PO -> B' = milieu A C :>PO -> C' = milieu A B :>PO -> triangle A' B' C'.
proof: Proof. intros. deroule_triangle A B C. red in |- *; intros; apply H3. assert (A' <> B'). apply (deux_milieux_distincts (A:=B) (B:=C) (C:=A)); auto with geo. halignes H7 k. apply colineaire_alignes with k; auto. rewrite <- (droite_milieu (A:=B) (B:=A) (C:=C) (I:=C') (J:=A')); auto with geo. rewrite <- (droite_milieu (A:=C) (B:=A) (C:=B) (I:=B') (J:=A')); auto with geo. VReplace (vec C' A') (mult_PP (-1) (vec A' C')). rewrite H9; Ringvec. Qed.