proposition: Lemma Rseq_cv_pos_infty_shift_compat : forall Un, Rseq_cv_pos_infty (Rseq_shift Un) -> Rseq_cv_pos_infty Un.
proof: Proof. intros Un H M. destruct (H M) as [N Hu]. exists (S N); intros n nSN. destruct n; [inversion nSN | ]. replace (Un (S n)) with (Rseq_shift Un n) by reflexivity. intuition (auto with arith). Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_usual_facts Lra