proposition: Lemma Rseq_cv_pos_infty_shifts_compat : forall Un N, Rseq_cv_pos_infty (Rseq_shifts Un N) -> Rseq_cv_pos_infty Un.
proof: Proof. intros Un N H M. destruct (H M) as [P HP]. exists (N + P)%nat; intros n nSN. assert (Hrew: (n = N + (n - N))%nat) by lia. rewrite Hrew ; apply HP ; lia. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_usual_facts Lra