proposition: Lemma argument_affixe_produit_positif_vecteur : forall (k : R) (A B A' B' : PO) (z z' : C), A <> B :>PO -> k > 0 -> vec A' B' = mult_PP k (vec A B) :>PP -> z = affixe_vec (vec A B) :>C -> z' = affixe_vec (vec A' B') :>C -> argument z' = argument z :>AV.
proof: Proof. intros k A B A' B' z z' H H0; try assumption. elim existence_representant_vecteur with (A := O) (B := A) (C := B); intros M; intros H1. elim existence_representant_vecteur with (A := O) (B := A') (C := B'); intros M'; intros H2. rewrite <- H2; rewrite <- H1; intros. apply (argument_affixe_produit_positif_vecteur_OM (k:=k) (M:=M) (M':=M') (z:=z) (z':=z')); auto. apply distinct_egalite_vecteur with (2 := H1); auto. Qed.