proposition: Lemma Series_le (a b : nat -> R) : (forall n : nat, 0 <= a n <= b n) -> ex_series b -> Series a <= Series b.
proof: Proof. move => Hn Hb. have Ha := (ex_series_le a b). apply Lim_seq_correct' in Ha. apply Lim_seq_correct' in Hb. move: Ha Hb ; apply is_lim_seq_le. elim => [ | n IH] /=. rewrite !sum_O. by apply Hn. rewrite !sum_Sn. apply Rplus_le_compat. by apply IH. by apply Hn. intros n. rewrite /norm /= /abs /= Rabs_pos_eq ; by apply Hn. by apply Hb. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy