proposition: Lemma distinct_produit_vecteur : forall (A B C : PO) (a : R), A <> B -> a <> 0 -> vec A C = mult_PP a (vec A B) :>PP -> A <> C.
proof: Proof. intros; red in |- *; intros. cut (~ (a = 0 \/ A = B)); intros. apply H3. apply produit_vecteur_nul. rewrite <- H1. rewrite H2; Ringvec. intuition. Qed.