proposition: Lemma paralleles_alignes3 : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> paralleles (droite A B) (droite C D) -> alignes C D A -> alignes A C B.
proof: Proof. intros A B C D H H0 H1 H2; try assumption. elim (paralleles_vecteur (A:=A) (B:=B) (C:=C) (D:=D)); intros; auto. discrimine C A. assert (alignes C A D); auto with geo. halignes H5 x0. rewrite H6 in H3. apply colineaire_alignes with (- (x * x0)). rewrite H3; Ringvec. Qed.