proposition: Lemma mes_alg_nulle : forall A B : PO, mes_alg A B = 0 :>R -> A = B.
proof: Proof. intros. apply vecteur_nul_conf. replace zero with (mult_PP 0 (vec A B)). apply def_mes_alg2. rewrite H; ring. unfold col_vec in |- *. exists 1. Ringvec. Ringvec. Qed.