proposition: Lemma le_limn_supD u v : bounded_fun u -> bounded_fun v -> limn_sup (u \+ v) <= limn_sup u + limn_sup v.
proof: Proof. move=> ba bb; have ab k : sups (u \+ v) k <= sups u k + sups v k. apply: sup_le_ub; first by exists ((u \+ v) k); exists k => /=. by move=> M [n /= kn <-]; apply: lerD; apply: sup_ub; [ exact/has_ubound_sdrop/bounded_fun_has_ubound; exact | exists n | exact/has_ubound_sdrop/bounded_fun_has_ubound; exact | exists n ]. have cu : cvgn (sups u). apply: nonincreasing_is_cvgn; last exact: bounded_fun_has_lbound_sups. exact/nonincreasing_sups/bounded_fun_has_ubound. have cv : cvgn (sups v). apply: nonincreasing_is_cvgn; last exact: bounded_fun_has_lbound_sups. exact/nonincreasing_sups/bounded_fun_has_ubound. rewrite -(limD cu cv); apply: ler_lim. - apply: nonincreasing_is_cvgn; last first. exact/bounded_fun_has_lbound_sups/bounded_funD. exact/nonincreasing_sups/bounded_fun_has_ubound/bounded_funD. - exact: is_cvgD cu cv. - exact: nearW. 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