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