proposition: Lemma infs_le_sups u n : cvgn u -> infs u n <= sups u n.
proof: Proof. move=> cu; rewrite /infs /sups /=; set A := sdrop _ _. have [a Aa] : A !=set0 by exists (u n); rewrite /A /=; exists n => //=. rewrite (@le_trans _ _ a) //; [apply/inf_lb|apply/sup_ub] => //. - exact/has_lbound_sdrop/bounded_fun_has_lbound/cvg_seq_bounded. - 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