proposition: Lemma paralleles_alignes : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> paralleles (droite A B) (droite C D) -> alignes A B C -> alignes A B D.
proof: Proof. intros. elim (paralleles_vecteur (A:=C) (B:=D) (C:=A) (D:=B)); intros; auto with geo. halignes H2 x0. apply colineaire_alignes with (x + x0). VReplace (vec A D) (add_PP (vec A C) (vec C D)). rewrite H3; rewrite H4; Ringvec. Qed.