proposition: Lemma is_LimSup_seq_scal_pos (a : R) (u : nat -> R) (l : Rbar) : (0 < a) -> is_LimSup_seq u l -> is_LimSup_seq (fun n => a * u n) (Rbar_mult a l).
proof: Proof. case: l => [l | | ] /= Ha Hu. move => eps. suff He : 0 < eps / a. case: (Hu (mkposreal _ He)) => {Hu} /= H1 H2 ; split. move => N ; case: (H1 N) => {H1} n [Hn H1]. exists n ; split. by []. rewrite (Rmult_comm _ (u n)) ; apply Rlt_div_l. by []. apply Rle_lt_trans with (2 := H1) ; right ; field ; by apply Rgt_not_eq. case: H2 => N H2. exists N => n Hn. rewrite (Rmult_comm _ (u n)) ; apply Rlt_div_r. by []. apply Rlt_le_trans with (1 := H2 _ Hn) ; right ; field ; by apply Rgt_not_eq. apply Rdiv_lt_0_compat ; [ by case eps | by [] ]. case: Rle_dec (Rlt_le _ _ Ha) => // H _. case: Rle_lt_or_eq_dec (Rlt_not_eq _ _ Ha) => {H} // _ _. move => M N. case: (Hu (M / a) N) => {Hu} n [Hn Hu]. exists n ; split. by []. rewrite (Rmult_comm _ (u n)) ; apply Rlt_div_l. by []. by []. case: Rle_dec (Rlt_le _ _ Ha) => // H _. case: Rle_lt_or_eq_dec (Rlt_not_eq _ _ Ha) => {H} // _ _. move => M. case: (Hu (M / a)) => {Hu} N Hu. exists N => n Hn. rewrite (Rmult_comm _ (u n)) ; apply Rlt_div_r. by []. by apply Hu. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy