proposition: Lemma is_cvg_sups u : cvgn u -> cvgn (sups u).
proof: Proof. move=> cf; have [M [Mreal Mu]] := cvg_seq_bounded cf. apply: nonincreasing_is_cvgn. exact/nonincreasing_sups/bounded_fun_has_ubound/cvg_seq_bounded. exists (- (M + 1)) => _ [n _ <-]; rewrite (@le_trans _ _ (u n)) //. by apply/lerNnormlW/Mu => //; rewrite ltrDl. apply: sup_ub; last by exists n => /=. exact/has_ubound_sdrop/bounded_fun_has_ubound/cvg_seq_bounded. 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