proposition: Lemma neq0_fine_cvgP a : a != 0 -> f @ F --> a%:E <-> fine \o f @ F --> a.
proof: Proof. move=> a_neq0; split=> [|Fa]; first exact: fine_cvg. apply: cvg_EFin=> //; near (0 : R)^'+ => e. have lea : e <= `|a| by near: e; apply: nbhs_right_le; rewrite normr_gt0. near=> x; have : `|a - fine (f x)| < e by near: x; apply: cvgr_dist_lt. by case: f=> //=; rewrite subr0; apply: contra_ltT. 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