proposition: Lemma EFin_lim (R : realFieldType) (f : nat -> R) : cvgn f -> limn (EFin \o f) = (limn f)%:E.
proof: Proof. move=> cf; apply: cvg_lim => //; move/cvg_ex : cf => [l fl]. by apply: (cvg_comp fl); rewrite (cvg_lim _ fl). 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