proposition: Lemma distinct_col_nonun : forall (A B C : PO) (x : R), B <> C -> vec A C = mult_PP x (vec A B) -> 1 + - x <> 0.
proof: Proof. intros. contrapose H. cut (x = 1); intros. apply vecteur_nul_conf. VReplace (vec B C) (add_PP (vec B A) (vec A C)). rewrite H0. subst_ x 1; Ringvec. RReplace x (x + 0). rewrite <- H1; ring. Qed.