proposition: Lemma lime_inf_ge0 f a : (forall x, 0 <= f x) -> 0 <= lime_inf f a.
proof: Proof. move=> f0; rewrite lime_inf_lim; apply: lime_ge; first exact: inf_ball_is_cvg. near=> b; rewrite inf_ballE. by apply: lb_ereal_inf => /= _ [r [abr/= ra]] <-; exact: f0. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)