proposition: Lemma mine_cvg_0_cvg_fin_num u x : 0 < x -> (forall k, 0 <= u k) -> mine (u n) x @[n --> \oo] --> 0 -> \forall n \near \oo, u n \is a fin_num.
proof: Proof. case: x => [r r0 u0 /fine_cvgP[_]|_ u0|//]; last first. under eq_cvg do rewrite miney. by case/fine_cvgP. move=> /cvgrPdist_lt/(_ _ r0)[N _ hN]. near=> n; have /hN : (N <= n)%N by near: n; exists N. rewrite sub0r normrN /= ger0_norm ?fine_ge0//; last first. by rewrite le_minr u0 ltW. by have := u0 n; case: (u n) => //=; rewrite ltxx. 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