proposition: Lemma quotient_mes_algebrique_vecteur : forall (A B C D : PO) (k : R), A <> B -> col_vec A B C D -> mes_alg C D / mes_alg A B = k -> vec C D = mult_PP k (vec A B).
proof: Proof. intros. apply def_mes_alg2; auto. assert (mes_alg A B <> 0). contrapose H. apply mes_alg_nulle; auto. RReplace (mes_alg C D) (mes_alg C D / mes_alg A B * mes_alg A B). rewrite H1; auto. field; auto. Qed.