proposition: Lemma Rser_cv_sig_shift_reciprocal_compat : forall Un, {l | Rser_cv (Rseq_shift Un) l} -> {l | Rser_cv Un l}.
proof: Proof. intros Un [l H]. exists (l + (Un O)). apply Rser_cv_shift_reciprocal. replace (l + Un 0%nat - Un 0%nat) with l by ring; assumption. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts MyNat MyRIneq PeanoNat Lra Rtactic