proposition: Lemma Rseq_cv_equiv_constant : forall Un l, l <> 0 -> Rseq_cv Un l -> Un ~ (Rseq_constant l).
proof: Proof. intros Un l Hl H. apply Rseq_equiv_sym. intros eps Heps. assert(Hpos : 0 < eps* Rabs l). pose proof (Rabs_pos_lt l Hl). apply Rmult_lt_0_compat; assumption. destruct (H (eps * (Rabs l))%R Hpos) as [N HN]. exists N. intros n Hn. unfold Rseq_minus, Rseq_constant. replace (l - Un n)%R with (- (Un n - l))%R by ring. rewrite Rabs_Ropp. left; apply HN; assumption. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra