proposition: Lemma mine_cvg_0_cvg_0 u x : 0 < x -> (forall k, 0 <= u k) -> mine (u n) x @[n --> \oo] --> 0 -> u n @[n --> \oo] --> 0.
proof: Proof. move=> x0 u0 h; apply/fine_cvgP; split. exact: (mine_cvg_0_cvg_fin_num x0). case: x x0 h => [r r0 h|_|//]; last first. under eq_cvg do rewrite miney. exact: fine_cvg. apply: (@minr_cvg_0_cvg_0 _ (fine \o u) r) => //. by move=> k /=; rewrite fine_ge0. exact: mine_cvg_minr_cvg. 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