proposition: Lemma argument_affixe_produit_negatif_vecteur_OM : forall (k : R) (M M' : PO) (z z' : C), O <> M :>PO -> k < 0 -> vec O M' = mult_PP k (vec O M) :>PP -> z = affixe_vec (vec O M) :>C -> z' = affixe_vec (vec O M') :>C -> argument z' = plus (argument z) (image_angle pi) :>AV.
proof: Proof. intros. cut (O <> M'); intros. rewrite (argument_def2 (M:=M) (z:=z)); auto with geo. rewrite (argument_def2 (M:=M') (z:=z')); auto with geo. apply angle_produit_negatif_r with k; auto with geo. apply distinct_produit_vecteur with (3 := H1); auto. auto with real. Qed.