proposition: Lemma inv_nonzero : forall z : C, z <> zeroC -> Cinv z <> zeroC.
proof: Proof. intros. apply nonzero_module. rewrite Cinv_module; auto with geo. cut (module z <> 0); intros; auto with geo. auto with real. Qed.