proposition: Lemma Rseq_cv_neg_infty_shift_compat_reciprocal : forall Un, Rseq_cv_neg_infty Un -> Rseq_cv_neg_infty (Rseq_shift Un).
proof: Proof. intros Un H M. destruct (H M) as [N Hu]. exists N; intros n nSN. unfold Rseq_shift. apply Hu. intuition. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_usual_facts Lra