proposition: Lemma minr_cvg_0_cvg_0 u r : 0 < r -> (forall k, 0 <= u k) -> minr (u n) r @[n --> \oo] --> 0 -> u n @[n --> \oo] --> 0.
proof: Proof. move=> r0 u0 minr_cvg; apply/cvgrPdist_lt => _ /posnumP[e]. have : 0 < minr e%:num r by rewrite lt_minr// r0 andbT. move/cvgrPdist_lt : minr_cvg => /[apply] -[M _ hM]. near=> n; rewrite sub0r normrN. have /hM : (M <= n)%N by near: n; exists M. rewrite sub0r normrN (ger0_norm (u0 n)) ger0_norm// => [/lt_min_lt//|]. by rewrite le_minr u0 ltW. 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