proposition: Lemma has_lbound_sdrop u : has_lbound (range u) -> forall m, has_lbound (sdrop u m).
proof: Proof. by move=> [M uM] n; exists M => _ [m /= nm] <-; rewrite uM //; exists m. 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