proposition: Lemma existence_module : forall z : C, exists r : R, module z = r.
proof: Proof. intros. elim existence_image_complexe with (z := z); intros M H1; try clear existence_image_complexe; try exact H1. exists (distance O M); eauto with geo. Qed.