proposition: Lemma Lim_seq_scal_l (u : nat -> R) (a : R) : Lim_seq (fun n => a * u n) = Rbar_mult a (Lim_seq u).
proof: Proof. case: (Req_dec a 0) => [ -> | Ha]. rewrite -(Lim_seq_ext (fun _ => 0)) /=. rewrite Lim_seq_const. case: (Lim_seq u) => [x | | ] //=. by rewrite Rmult_0_l. case: Rle_dec (Rle_refl 0) => // H _. case: Rle_lt_or_eq_dec (Rlt_irrefl 0) => // _ _. case: Rle_dec (Rle_refl 0) => // H _. case: Rle_lt_or_eq_dec (Rlt_irrefl 0) => // _ _. move => n ; by rewrite Rmult_0_l. wlog: a u Ha / (0 < a) => [Hw | {} Ha]. case: (Rlt_le_dec 0 a) => Ha'. by apply Hw. case: Ha' => // Ha'. rewrite -(Lim_seq_ext (fun n => - a * - u n)). rewrite -Rbar_mult_opp. rewrite -Lim_seq_opp. apply Hw. contradict Ha ; rewrite -(Ropp_involutive a) Ha ; ring. apply Ropp_lt_cancel ; by rewrite Ropp_0 Ropp_involutive. move => n ; ring. rewrite /Lim_seq. rewrite {2}/LimSup_seq ; case: ex_LimSup_seq => ls Hs ; rewrite {2}/LimInf_seq ; case: ex_LimInf_seq => li Hi ; simpl proj1_sig. apply (is_LimSup_seq_scal_pos a) in Hs => //. apply (is_LimInf_seq_scal_pos a) in Hi => //. rewrite (is_LimSup_seq_unique _ _ Hs). rewrite (is_LimInf_seq_unique _ _ Hi). case: ls {Hs} => [ls | | ] ; case: li {Hi} => [li | | ] //= ; case: (Rle_dec 0 a) (Rlt_le _ _ Ha) => // Ha' _ ; case: (Rle_lt_or_eq_dec 0 a Ha') (Rlt_not_eq _ _ Ha) => //= _ _ ; apply f_equal ; field. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy