proposition: Lemma Rser_pos_maj_cv : forall (An Bn : nat -> R), (forall n : nat, 0 <= An n) -> (forall n : nat, 0 <= Bn n) -> Rseq_le An Bn -> {l | Rser_cv Bn l } -> {l | Rser_cv An l}.
proof: Proof. intros An Bn An_pos Bn_pos AnBn [lb Hlb] ; apply Rser_pos_bound_cv with lb. assumption. intro n ; transitivity (Rseq_sum Bn n). apply Rseq_sum_le_compat ; assumption. apply growing_ineq ; [apply Rser_pos_growing |] ; assumption. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts MyNat MyRIneq PeanoNat Lra Rtactic