proposition: Lemma is_LimInf_seq_scal_pos (a : R) (u : nat -> R) (l : Rbar) : (0 < a) -> is_LimInf_seq u l -> is_LimInf_seq (fun n => a * u n) (Rbar_mult a l).
proof: Proof. move => Ha Hu. apply is_LimSup_opp_LimInf_seq in Hu. apply is_LimSup_opp_LimInf_seq. replace (Rbar_opp (Rbar_mult a l)) with (Rbar_mult a (Rbar_opp l)). apply is_LimSup_seq_ext with (fun n => a * - u n). move => n ; ring. by apply is_LimSup_seq_scal_pos. case: (l) => [x | | ] /=. apply f_equal ; ring. case: Rle_dec (Rlt_le _ _ Ha) => // H _. case: Rle_lt_or_eq_dec (Rlt_not_eq _ _ Ha) => // H _. case: Rle_dec (Rlt_le _ _ Ha) => // H _. case: Rle_lt_or_eq_dec (Rlt_not_eq _ _ Ha) => // H _. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy