proposition: Lemma Rseq_equiv_cv_constant : forall Un l, Un ~ (Rseq_constant l) -> Rseq_cv Un l.
proof: Proof. intros Un l H. apply Rseq_equiv_sym in H. assert(Rseq_cv (Un - l) 0). apply Rseq_little_O_cv with (Vn := l) (l := l). intros eps Heps. destruct (H eps Heps) as [N HN]. exists N. intros n Hn; unfold Rseq_minus, Rseq_constant. replace (Un n - l)%R with (-(l - Un n))%R by ring. rewrite Rabs_Ropp. apply HN; assumption. apply Rseq_constant_cv. replace l with (0 + l)%R by ring. apply Rseq_cv_eq_compat with ((Un - l) + l). intro n; unfold Rseq_minus, Rseq_constant, Rseq_plus; ring. auto with Rseq. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra