proposition: Lemma Cinv_module : forall z : C, z <> zeroC -> module (Cinv z) = / module z.
proof: Proof. intros. cut (module z * module (Cinv z) = 1); intros. cut (module z <> 0); intros; auto with geo. apply Rmult_eq_reg_l with (module z); auto. rewrite H0; auto with real. rewrite <- Cmult_module; rewrite Cinv_def; auto with geo. Qed.