proposition: Lemma limn_supD u v : cvgn u -> cvgn v -> limn_sup (u \+ v) = limn_sup u + limn_sup v.
proof: Proof. move=> cu cv; have [ba bb] := (cvg_seq_bounded cu, cvg_seq_bounded cv). apply/eqP; rewrite eq_le le_limn_supD //=. have := @le_limn_supD _ _ (bounded_funD ba bb) (bounded_funN bb). rewrite -lerBlDr; apply: le_trans. rewrite -[_ \+ _]/(u + v - v) addrK -limn_infN; last exact: is_cvgN. rewrite /comp /=; under eq_fun do rewrite opprK. by rewrite lerD// cvg_limn_infE// cvg_limn_supE. 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