proposition: Lemma maxe_cvg_maxr_cvg u r : (r < 0)%R -> (forall k, u k <= 0) -> maxe (u n) r%:E @[n --> \oo] --> 0 -> maxr (fine (u n)) r @[n --> \oo] --> 0%R.
proof: Proof. rewrite -[in (r < _)%R]oppr0 ltrNr => r0 u0. under eq_fun do rewrite -(oppeK (u _)) -[in maxe _ _](oppeK r%:E) -oppe_min. rewrite -[in _ --> _]oppe0 => /cvgeNP/mine_cvg_minr_cvg-/(_ r0). have Nu0 k : 0 <= - u k by rewrite leeNr oppe0. move=> /(_ Nu0)/(cvgNP _ _).2; rewrite oppr0. by under eq_cvg do rewrite /GRing.opp /= oppr_min fineN !opprK. 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