proposition: Lemma Rseq_limit_comparison: forall (An Bn : nat -> R) (a b : R), (forall n, An n <= Bn n) -> Rseq_cv An a -> Rseq_cv Bn b -> a <= b.
proof: Proof. intros An Bn a b Hcomp Ha Hb. assert (0 <= b - a). apply Rseq_positive_limit with (fun n => (Bn n - An n)%R). intro n; pose proof Hcomp n; lra. apply Rseq_cv_minus_compat; auto. lra. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra