proposition: Lemma colineaire_alignes : forall (k : R) (A B C : PO), vec A C = mult_PP k (vec A B) -> alignes A B C.
proof: Proof. unfold alignes in |- *; intros. right; try assumption. apply colineaire_alignes1 with k; auto. Qed.