proposition: Lemma distinct_mult_vecteur : forall (A B C D : PO) (a : R), A <> B :>PO -> a <> 0 :>R -> vec C D = mult_PP a (vec A B) :>PP -> C <> D :>PO.
proof: Proof. intros. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := a); intros E H2; try clear existence_representant_mult_vecteur; try exact H2. cut (A <> E); intros. apply distinct_egalite_vecteur with (1 := H3); auto. rewrite H1; auto. apply distinct_produit_vecteur with (3 := H2); auto. Qed.