proposition: Lemma bounded_fun_has_lbound_sups u : bounded_fun u -> has_lbound (range (sups u)).
proof: Proof. move=> /[dup] ba /bounded_fun_has_lbound/has_lbound_sdrop h. have [M hM] := h O; exists M => y [n _ <-]. rewrite (@le_trans _ _ (u n)) //; first by apply: hM; exists n. apply: sup_ub; last by exists n => /=. by move: ba => /bounded_fun_has_ubound/has_ubound_sdrop; exact. 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