proposition: Lemma lime_inf_sup f a : lime_inf f a <= lime_sup f a.
proof: Proof. rewrite lime_inf_lim lime_sup_lim; apply: lee_lim => //. near=> r. rewrite ereal_sup_le//. have ? : exists2 x, ball a r x /\ x <> a & f x = f (a + r / 2)%R. exists (a + r / 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. by exists (f (a + r / 2)%R) => //=; rewrite inf_ballE ereal_inf_lb. 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)