proposition: Lemma limn_infN u : cvgn u -> limn_inf (-%R \o u) = - limn_sup u.
proof: Proof. by move=> cu_; rewrite /limn_inf infsN limN//; exact: is_cvg_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