proposition: Lemma paralleles_alignes1 : forall A B C D E F : PO, A <> B :>PO -> C <> D :>PO -> vec E F = vec A B :>PP -> paralleles (droite A B) (droite C D) -> alignes C D E -> alignes C D F.
proof: Proof. intros A B C D E F H H0 H1 H2 H3; try assumption. elim (paralleles_vecteur (A:=A) (B:=B) (C:=C) (D:=D)); intros; auto. halignes H3 x0. apply colineaire_alignes with (x0 + x). VReplace (vec C F) (add_PP (vec C E) (vec E F)). rewrite H5; rewrite H1; rewrite H4. Ringvec. Qed.