proposition: Lemma cvg_seq_bounded {V : normedModType K} (a : nat -> V) : cvgn a -> bounded_fun a.
proof: Proof. move=> /cvg_bounded/ex_bound => -[/= Moo] => -[N _ /(_ _) aM]. have Moo_real : Moo \is Num.real by rewrite ger0_real ?(le_trans _ (aM N _))/=. rewrite /bounded_near /=; near=> M => n _. have [nN|nN]/= := leqP N n; first by apply: (le_trans (aM _ _)). move: n nN; suff /(_ (Ordinal _)) : forall n : 'I_N, `|a n| <= M by []. by near: M; apply: filter_forall => i; apply: nbhs_pinfty_ge. 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