proposition: Lemma limn_einf_sup u : limn_einf u <= limn_esup u.
proof: Proof. rewrite limn_esup_lim limn_einf_lim. apply: lee_lim; [exact/is_cvg_einfs|exact/is_cvg_esups|]. by apply: nearW; exact: einfs_le_esups. 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