proposition: Lemma nondecreasing_infs u : has_lbound (range u) -> nondecreasing_seq (infs u).
proof: Proof. move=> u_lb; rewrite -nonincreasing_opp -supsN; apply/nonincreasing_sups. by move: u_lb => /has_lb_ubN; rewrite /comp /= image_comp. 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