proposition: Lemma cvg_restrict f u_ l : ([sequence if (n <= N)%N then f n else u_ n]_n @ \oo --> l) = (u_ @ \oo --> l).
proof: Proof. rewrite propeqE; split; apply: cvg_trans; apply: near_eq_cvg; by near do [move=> /=; case: ifP => //; rewrite ltn_geF//]. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau