proposition: Lemma module_pos : forall z : C, module z >= 0.
proof: Proof. intros. elim existence_image_complexe with (z := z); intros M H; try clear existence_image_complexe; try exact H. rewrite (module_def H); auto with geo. Qed.