proposition: Lemma limn_inf_sup u : cvgn u -> limn_inf u <= limn_sup u.
proof: Proof. move=> cf_; apply: ler_lim; [exact: is_cvg_infs|exact: is_cvg_sups|]. by apply: nearW => n; apply: infs_le_sups. 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