proposition: Lemma triangle_droite_milieu_paralleles : forall A B C A' B' : PO, triangle A B C -> A' = milieu B C :>PO -> B' = milieu A C :>PO -> paralleles (droite A B) (droite A' B').
proof: Proof. intros A B C A' B' H H0 H1; try assumption. deroule_triangle A B C. apply colineaires_paralleles with (-2); auto. apply (deux_milieux_distincts (A:=B) (B:=C) (C:=A)); auto with geo. rewrite <- (droite_milieu (A:=C) (B:=A) (C:=B) (I:=B') (J:=A')); auto with geo. Ringvec. Qed.