proposition: Lemma module_nul_zeroC : forall z : C, module z = 0 -> z = zeroC.
proof: Proof. intros. elim existence_image_complexe with (z := z); intros M H1; try clear existence_image_complexe; try exact H1. cut (O = M); intros. rewrite (affixe_image H1). rewrite <- H0; auto with geo. apply distance_refl1. rewrite <- H; symmetry in |- *; auto with geo. Qed.