proposition: Lemma vecteur_egalite_point : forall (a : R) (A B : PO), mult_PP a (vec A B) = zero -> a <> 0 -> A = B.
proof: Proof. intros a A B H H0; try assumption. generalize produit_vecteur_nul; intros. elim H1 with (a := a) (A := A) (B := B); [ intros H2; try clear H1 | intros H2; try clear H1; try exact H2 | try clear H1 ]. absurd (a = 0); auto. auto. Qed.