proposition: Lemma inv_continuous (x : K) : x != 0 -> {for x, continuous (@GRing.inv K)}.
proof: Proof. move=> x_neq0; have nx_gt0 : `|x| > 0 by rewrite normr_gt0. apply/(@cvgrPdist_ltp _ _ _ (nbhs x)); near (0 : K)^'+ => d. near=> e. near=> y; have y_neq0 : y != 0 by near: y; apply: (cvgr_neq0 x). rewrite /= -div1r -[y^-1]div1r -mulNr addf_div// mul1r mulN1r normrM normfV. rewrite ltr_pdivrMr ?normr_gt0 ?mulf_neq0// (@lt_le_trans _ _ (e * d))//. by near: y; apply: cvgr_distC_lt => //; rewrite mulr_gt0. rewrite ler_pM2l => //=; rewrite normrM -ler_pdivrMl//. near: y; apply: (cvgr_norm_ge x) => //; rewrite ltr_pdivrMl//. by near: d; apply: nbhs_right_lt; rewrite mulr_gt0. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule