proposition: Lemma cvg_lim {U : Type} {F} {FF : ProperFilter F} (f : U -> T) (l : T) : f @ F --> l -> lim (f @ F) = l.
proof: Proof. by move=> /[dup] /cvgP /cvg_unique; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed