proposition: Lemma colineaire_mes_alg_conf : forall (A B C D : PO) (k : R), A <> B -> col_vec A B A C -> col_vec A B A D -> mes_alg A C = k * mes_alg A B -> mes_alg A D = k * mes_alg A B -> C = D.
proof: Proof. intros. assert (vec A C = mult_PP k (vec A B)); auto with geo. assert (vec A D = mult_PP k (vec A B)); auto with geo. apply vecteur_nul_conf. VReplace (vec C D) (add_PP (vec A D) (mult_PP (-1) (vec A C))). rewrite H5; rewrite H4; Ringvec. Qed.