proposition: Lemma distinct_col_nonzero : forall (A B C D : PO) (x : R), A <> B -> vec A B = mult_PP x (vec C D) -> x <> 0.
proof: Proof. intros. contrapose H. apply vecteur_nul_conf. rewrite H0; rewrite H1. Ringvec. Qed.