proposition: Lemma lime_sup_lim f a : lime_sup f a = lim (sup_ball f a e @[e --> 0^'+]).
proof: Proof. apply/eqP; rewrite eq_le; apply/andP; split. apply: lime_ge => //; near=> e; apply: ereal_inf_lb => /=. by exists (ball a e `\ a) => //=; exact: dnbhs_ball. apply: lb_ereal_inf => /= _ [A [r /= r0 arA] <-]. apply: lime_le => //; near=> e. apply: le_ereal_sup => _ [s [ase /eqP sa] <- /=]. exists s => //; apply: arA => //=; apply: (lt_le_trans ase). by near: e; exact: nbhs_right_le. 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)