proposition: Lemma vecteur_quotient_mes_algebrique : forall (A B C D : PO) (k : R), A <> B -> vec C D = mult_PP k (vec A B) -> mes_alg C D / mes_alg A B = k.
proof: Proof. intros. rewrite (def_mes_alg H0); auto. field. contrapose H. apply mes_alg_nulle; auto. Qed.