proposition: Lemma Rser_pos_maj_cv_shift : forall Un Vn : nat -> R, (forall n, 0 <= Un (S n) <= Vn n) -> {lv : R | Rser_cv Vn lv} -> {lu : R | Rser_cv Un lu}.
proof: Proof. intros Un Vn uposmaj Vncv. apply Rser_cv_sig_shift_reciprocal_compat. eapply Rser_pos_maj_cv. intro; unfold Rseq_shift; apply (uposmaj n). intro; eapply Rle_trans; apply (uposmaj n). intro; apply (uposmaj n). assumption. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts MyNat MyRIneq PeanoNat Lra Rtactic