proposition: Lemma Rseq_constant_cv : forall r, Rseq_cv (Rseq_constant r) r.
proof: Proof. intros r eps Heps; exists O; intros n Hn. unfold R_dist; unfold Rseq_constant. replace (r - r)%R with 0 by ring. rewrite Rabs_R0; apply Heps. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra