fact: Definition lim_sup_bdd (a : ℕ → ℝ) (pr1 : has_ub a) (pr2 : has_lb (sequence_ub a pr1)) := decreasing_cv (sequence_ub a pr1) (Wn_decreasing a pr1) (pr2).
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type Automation Libs.Analysis.Sequences Libs.Analysis.Subsequences Libs.Analysis.SupAndInf Libs.Analysis.SequentialAccumulationPoints Notations Tactics