proposition: Lemma nonincreasing_sups u : has_ubound (range u) -> nonincreasing_seq (sups u).
proof: Proof. move=> u_ub m n mn; apply: le_sup => [_ /= [p np] <-| |]. - by apply/downP; exists (u p) => //=; exists p => //; exact: leq_trans np. - by exists (u n) => /=; exists n => /=. - by split; [exists (u m); exists m => //=|exact/has_ubound_sdrop]. 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