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