proposition: Lemma lime_sup_ge0 f a : (forall x, 0 <= f x) -> 0 <= lime_sup f a.
proof: Proof. move=> f0; rewrite lime_supE; apply: lb_ereal_inf => /= x [e /=]. rewrite in_itv/= andbT => e0 <-{x}; rewrite -(ereal_sup1 0) ereal_sup_le //=. exists (f (a + e / 2)%R); last by rewrite ereal_sup1 f0. exists (a + e / 2)%R => //=; split. rewrite /ball/= opprD addrA subrr sub0r normrN gtr0_norm ?divr_gt0//. by rewrite ltr_pdivrMr// ltr_pMr// ltr1n. by apply/eqP; rewrite gt_eqF// ltr_pwDr// divr_gt0. 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)