proposition: Lemma alignes_trans2 : forall A B C D : PO, A <> B -> alignes A B C -> alignes A B D -> alignes B C D.
proof: Proof. intros. assert (alignes B A D); auto with geo. halignes H2 k. assert (A = B); auto. tauto. assert (alignes B C A); auto with geo. halignes H4 k0. apply colineaire_alignes with (k * k0). rewrite H3; rewrite H5. Ringvec. Qed.