proposition: Lemma einfs_le_esups u n : einfs u n <= esups u n.
proof: Proof. rewrite /einfs /=; set A := sdrop _ _; have [a Aa] : A !=set0. by exists (u n); rewrite /A /=; exists n => //=. by rewrite (@le_trans _ _ a) //; [exact/ereal_inf_lb|exact/ereal_sup_ub]. Unshelve. all: by end_near. 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