proposition: Lemma Rseq_interval_compat : forall (An : Rseq) (a lb ub : R), (forall n, interval lb ub (An n)) -> Rseq_cv An a -> interval lb ub a.
proof: Proof. intros An a lb ub Hcomp Ha ; split ; eapply Rseq_limit_comparison. intro ; apply (proj1 (Hcomp n)). apply Rseq_constant_cv. assumption. intro n ; apply (proj2 (Hcomp n)). assumption. apply Rseq_constant_cv. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra