proposition: Lemma Series_scal_l (c : R) (a : nat -> R) : Series (fun n => c * a n) = c * Series a.
proof: Proof. rewrite /Series. have H0 : (forall x, c * Rbar.real x = Rbar.real (Rbar.Rbar_mult (Rbar.Finite c) x)). case: (Req_dec c 0) => [-> | Hk]. case => [x | | ] //= ; rewrite Rmult_0_l. case: Rle_dec (Rle_refl 0) => //= H0 _. case: Rle_lt_or_eq_dec (Rlt_irrefl 0) => //= _ _. case: Rle_dec (Rle_refl 0) => //= H0 _. case: Rle_lt_or_eq_dec (Rlt_irrefl 0) => //= _ _. case => [x | | ] //= ; rewrite Rmult_0_r. case: Rle_dec => //= H0. case: Rle_lt_or_eq_dec => //=. case: Rle_dec => //= H0. case: Rle_lt_or_eq_dec => //=. rewrite H0 -(Lim_seq_scal_l _ c). apply f_equal, Lim_seq_ext. elim => [ | n IH]. rewrite !sum_O ; ring. rewrite !sum_Sn IH /plus /=. ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy