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