proposition: Lemma permute_alignes : forall A B C : PO, alignes A B C -> alignes B A C.
proof: Proof. intros. halignes H x. apply colineaire_alignes with (1 + - x). VReplace (vec B C) (add_PP (vec B A) (vec A C)). rewrite H0; Ringvec. Qed.