proposition: Lemma alignes1_colineaire : forall A B C : PO, alignes1 A B C -> col_vec A B A C.
proof: Proof. unfold alignes1, vec, col_vec in |- *; intros. elim H; intros k H0; try clear H; try exact H0. exists (1 + - k); auto. unfold vec in |- *; rewrite H0. RingPP. Qed.