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