proposition: Lemma maxe_cvg_0_cvg_0 u x : x < 0 -> (forall k, u k <= 0) -> maxe (u n) x @[n --> \oo] --> 0 -> u n @[n --> \oo] --> 0.
proof: Proof. rewrite -[in x < _]oppe0 lteNr => x0 u0. under eq_fun do rewrite -(oppeK (u _)) -[in maxe _ _](oppeK x) -oppe_min. rewrite -[in _ --> _]oppe0 => /cvgeNP/mine_cvg_0_cvg_0-/(_ x0). have Nu0 k : 0 <= - u k by rewrite leeNr oppe0. by move=> /(_ Nu0); rewrite -[in _ --> _]oppe0 => /cvgeNP. 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