proposition: Lemma nboundedP u : reflect (exists2 M, 0 < M & forall n, `|u n| < M) `[< nbounded u >].
proof: Proof. apply: (iffP idP) => [/asboolP[]|]; first elim/nbh_finW. move=> M /= gt0_M cv; exists M => [|n] //. by have := cv n; rewrite inE subr0. case=> M _ cv; apply/asboolP; exists (B 0 M) => n; rewrite inE subr0. by rewrite eclamp_id // (@le_lt_trans _ _ `|u 0%N|). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.bigenough.bigenough mathcomp.classical(boolp classical_sets functions) mathcomp.classical(mathcomp_extra) xfinmap ereal reals discrete topology