proposition: Lemma module_affixe_produit_vecteur_OM : forall (k : R) (M M' : PO) (z z' : C), vec O M' = mult_PP k (vec O M) :>PP -> z = affixe_vec (vec O M) :>C -> z' = affixe_vec (vec O M') :>C -> module z' = Rabs k * module z.
proof: Proof. intros. rewrite (module_def2 (z:=z) (M:=M)); auto with geo. rewrite (module_def2 (z:=z') (M:=M')); auto with geo. Qed.